# HG changeset patch
# User haftmann
# Date 1556707240 0
# Node ID 129757af1096fde913cc64247aa3f9db05302250
# Parent  3706106c2e0f2092f7a98210dd259ff792570d7f
more correct simulation of eigen context for generated Isar statements

diff -r 3706106c2e0f -r 129757af1096 src/HOL/ex/Sketch_and_Explore.thy
--- a/src/HOL/ex/Sketch_and_Explore.thy	Wed May 01 14:38:42 2019 +0100
+++ b/src/HOL/ex/Sketch_and_Explore.thy	Wed May 01 10:40:40 2019 +0000
@@ -34,9 +34,19 @@
   |> Sledgehammer_Util.simplify_spaces
   |> maybe_quote ctxt;
 
-fun print_isar_skeleton ctxt indent keyword (fixes, assms, concl) =
+fun eigen_context_for_statement (fixes, assms, concl) ctxt =
   let
-    val (_, ctxt') = Variable.add_fixes (map fst fixes) ctxt;
+    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;
+
+fun print_isar_skeleton ctxt indent keyword stmt =
+  let
+    val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt;
     val prefix = replicate_string indent " ";
       \<comment> \<open>TODO consider pre-existing indentation -- how?\<close>
     val prefix_sep = "\n" ^ prefix ^ "    and ";