# HG changeset patch
# User Simon Wimmer <wimmers@in.tum.de>
# Date 1713455594 -7200
# Node ID 0c51e0a6bc378d04c575d2ab52f65bf4e85be3d0
# Parent  12ce957231e0b335a2b26179dbd16cf073a21dea
sketch & explore: recover from duplicate fixed variables in Isar proofs

diff -r 12ce957231e0 -r 0c51e0a6bc37 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Thu Apr 18 13:06:48 2024 +0200
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Thu Apr 18 17:53:14 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 =