# HG changeset patch
# User wenzelm
# Date 1713622020 -7200
# Node ID 5972799988afaf410eb55940c0d0679d8a4058c9
# Parent  bc450c8754ef7b5f5df292dcca5f563f2f9c998d
clone of 0c51e0a6bc37;

diff -r bc450c8754ef -r 5972799988af src/HOL/ex/Sketch_and_Explore.thy
--- 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 =