diff --git a/tools/autocorres/TypHeapSimple.thy b/tools/autocorres/TypHeapSimple.thy
index fa3a1492f..e21af2afb 100644
--- a/tools/autocorres/TypHeapSimple.thy
+++ b/tools/autocorres/TypHeapSimple.thy
@@ -106,7 +106,7 @@ lemma if_eqI:
   by simp
 
 lemma heap_type_tag_ptr_retyp:
-    "snd (s (ptr_val t)) = empty \<Longrightarrow>
+    "snd (s (ptr_val t)) = Map.empty \<Longrightarrow>
         heap_type_tag (ptr_retyp (t :: 'a::mem_type ptr) s) (ptr_val t) = HeapType (typ_uinfo_t TYPE('a))"
   apply (unfold ptr_retyp_def heap_type_tag_def)
   apply (subst htd_update_list_index, fastforce, fastforce)+
@@ -126,7 +126,7 @@ lemma not_snd_last_typ_slice_t:
   by (case_tac z, clarsimp)
 
 lemma heap_type_tag_ptr_retyp_rest:
-    "\<lbrakk> snd (s (ptr_val t + k)) = empty; 0 < k; unat k < size_td (typ_uinfo_t TYPE('a)) \<rbrakk> \<Longrightarrow>
+    "\<lbrakk> snd (s (ptr_val t + k)) = Map.empty; 0 < k; unat k < size_td (typ_uinfo_t TYPE('a)) \<rbrakk> \<Longrightarrow>
         heap_type_tag (ptr_retyp (t :: 'a::mem_type ptr) s) (ptr_val t + k) = HeapFootprint"
   apply (unfold ptr_retyp_def heap_type_tag_def)
   apply (subst htd_update_list_index, simp, clarsimp,
diff --git a/tools/autocorres/autocorres_trace.ML b/tools/autocorres/autocorres_trace.ML
index 315544ab4..b271cad15 100644
--- a/tools/autocorres/autocorres_trace.ML
+++ b/tools/autocorres/autocorres_trace.ML
@@ -350,7 +350,7 @@ fun dropQuotes s = if String.isPrefix "\"" s andalso String.isSuffix "\"" s
                        then String.substring (s, 1, String.size s - 2) else s
 
 fun cterm_to_string no_markup =
-  Proof_Display.pp_cterm Thy_Info.pure_theory
+  Proof_Display.pp_cterm (fn _ => @{theory Pure})
   #> Pretty.string_of
   #> YXML.parse_body
   #> (if no_markup then XML.content_of else YXML.string_of_body)
diff --git a/tools/autocorres/heap_lift.ML b/tools/autocorres/heap_lift.ML
index 42c13fa11..833833a77 100644
--- a/tools/autocorres/heap_lift.ML
+++ b/tools/autocorres/heap_lift.ML
@@ -137,7 +137,7 @@ end
 (* The opposite to "mk_first_order" *)
 fun dest_first_order ctxt ct =
   Conv.bottom_conv (K (Conv.try_conv (Conv.rewr_conv
-    @{lemma "(op $) == (%a b. a b)" by (rule meta_ext, rule ext, simp)}))) ctxt ct
+    @{lemma "($) == (%a b. a b)" by (rule meta_ext, rule ext, simp)}))) ctxt ct
 
 (*
  * Resolve "base_thm" with "subgoal_thm" in all assumptions it is possible to
diff --git a/tools/autocorres/trace_antiquote.ML b/tools/autocorres/trace_antiquote.ML
index c4928c5e0..c48343405 100644
--- a/tools/autocorres/trace_antiquote.ML
+++ b/tools/autocorres/trace_antiquote.ML
@@ -23,7 +23,7 @@ struct
 val tracing_str =
   "(fn x => (Pretty.writeln (Pretty.enum \" \" \"\" \"\" ["
     ^ "Pretty.str \"Trace:\", (Pretty.from_ML (ML_Pretty.from_polyml ("
-      ^ "ML_system_pretty (x, ML_Print_Depth.get_print_depth ()))))])))"
+      ^ "ML_system_pretty (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ())))))])))"
 
 val _ = Theory.setup (ML_Antiquotation.inline (Binding.name "trace") (Scan.succeed tracing_str))