# HG changeset patch # User Simon Wimmer # 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