# HG changeset patch
# User Simon Wimmer <wimmers@in.tum.de>
# Date 1710187883 -3600
# Node ID 0d5c41ea208ab9032c16f5d9f08dc1b7efd7ffa6
# Parent  54e9875e491f3644db9967e96fa25ddfe0e9aa1c
sketch & explore: reduce unnecessary type constraints

diff -r 54e9875e491f -r 0d5c41ea208a src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:20:36 2024 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Mon Mar 11 21:11:23 2024 +0100
@@ -31,15 +31,11 @@
   |> Sledgehammer_Util.simplify_spaces
   |> ATP_Util.maybe_quote ctxt;
 
-fun eigen_context_for_statement (fixes, assms, concl) ctxt =
+fun eigen_context_for_statement (params, assms, concl) ctxt =
   let
-    val (fixes', ctxt') = Variable.add_fixes (map fst fixes) ctxt;
-    val subst_free = AList.lookup (op =) (map fst fixes ~~ fixes')
-    val subst = map_aterms (fn Free (v, T) => Free (the_default v (subst_free v), T)
-      | t => t)
-    val assms' = map subst assms;
-    val concl' = subst concl;
-  in ((fixes, assms', concl'), ctxt') end;
+    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
+  in ((params, assms, concl), ctxt') end;
 
 fun print_isar_skeleton ctxt indent keyword stmt =
   let