--- a/src/HOL/ex/Sketch_and_Explore.thy Thu Apr 18 15:20:24 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy Sat Apr 20 16:07:00 2024 +0200
@@ -34,6 +34,8 @@
let
val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
val ctxt' = ctxt |> Variable.set_body false |> Proof_Context.add_fixes fixes |> snd
+ handle ERROR _ =>
+ ctxt |> Variable.set_body true |> Proof_Context.add_fixes fixes |> snd
in ((params, assms, concl), ctxt') end;
fun print_isar_skeleton ctxt indent keyword stmt =