# HG changeset patch
# User wenzelm
# Date 1559564781 -7200
# Node ID 61621dc439d4a52c87ccb4a7d85192aa5632343f
# Parent  959e167798f01d3c8830c2e885a908f6055dadfe
clarified context: prefer abstract Variable.auto_fixes;

diff -r 959e167798f0 -r 61621dc439d4 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Jun 03 13:49:35 2019 +0200
+++ b/src/Pure/Isar/local_defs.ML	Mon Jun 03 14:26:21 2019 +0200
@@ -249,15 +249,22 @@
       |> (snd o Logic.dest_equals o Thm.prop_of)
       |> conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt get_pos);
-    fun prove def_ctxt def =
-      Goal.prove def_ctxt
-        ((not (Variable.is_body def_ctxt) ? Variable.add_free_names def_ctxt prop) []) [] prop
-        (fn {context = goal_ctxt, ...} =>
-          ALLGOALS
-            (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
-              rewrite_goal_tac goal_ctxt [def] THEN'
-              resolve_tac goal_ctxt [Drule.reflexive_thm]))
-      handle ERROR msg => cat_error msg "Failed to prove definitional specification";
+    fun prove def_ctxt0 def =
+      let
+        val def_ctxt = Variable.auto_fixes prop def_ctxt0;
+        val def_thm =
+          Goal.prove def_ctxt [] [] prop
+            (fn {context = goal_ctxt, ...} =>
+              ALLGOALS
+                (CONVERSION (meta_rewrite_conv goal_ctxt) THEN'
+                  rewrite_goal_tac goal_ctxt [def] THEN'
+                  resolve_tac goal_ctxt [Drule.reflexive_thm]))
+          handle ERROR msg => cat_error msg "Failed to prove definitional specification";
+      in
+        def_thm
+        |> singleton (Variable.export def_ctxt def_ctxt0)
+        |> Drule.zero_var_indexes
+      end;
   in (((c, T), rhs), prove) end;
 
 end;