# HG changeset patch
# User wenzelm
# Date 1163539021 -3600
# Node ID d9dd7b4e5e69feae2a815c0368cabe02de45a65b
# Parent  6cca4865e3881b779d9a33ea8c97c1510012ee98
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);

diff -r 6cca4865e388 -r d9dd7b4e5e69 TFL/rules.ML
--- a/TFL/rules.ML	Tue Nov 14 22:17:00 2006 +0100
+++ b/TFL/rules.ML	Tue Nov 14 22:17:01 2006 +0100
@@ -816,7 +816,7 @@
 fun prove strict (ptm, tac) =
   let
     val {thy, t, ...} = Thm.rep_cterm ptm;
-    val ctxt = ProofContext.init thy |> Variable.fix_frees t;
+    val ctxt = ProofContext.init thy |> Variable.auto_fixes t;
   in
     if strict then Goal.prove ctxt [] [] t (K tac)
     else Goal.prove ctxt [] [] t (K tac)
diff -r 6cca4865e388 -r d9dd7b4e5e69 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Nov 14 22:17:00 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Nov 14 22:17:01 2006 +0100
@@ -869,7 +869,7 @@
         val ts = maps (map #1 o #2) asms';
         val (ps, qs) = chop (length ts) axs;
         val (_, ctxt') =
-          ctxt |> fold Variable.fix_frees ts
+          ctxt |> fold Variable.auto_fixes ts
           |> ProofContext.add_assms_i (axioms_export (if ax_in_ctxt then ps else [])) asms';
       in ((ctxt', Assumed qs), []) end
   | activate_elem _ _ ((ctxt, Derived ths), Assumes asms) =
@@ -881,7 +881,7 @@
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
             in (t', ((Thm.def_name_optional c name, atts), [(t', ps)])) end);
         val (_, ctxt') =
-          ctxt |> fold (Variable.fix_frees o #1) asms
+          ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
       in ((ctxt', Assumed axs), []) end
   | activate_elem _ _ ((ctxt, Derived ths), Defines defs) =
diff -r 6cca4865e388 -r d9dd7b4e5e69 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Nov 14 22:17:00 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Nov 14 22:17:01 2006 +0100
@@ -921,8 +921,7 @@
 (* fixes vs. frees *)
 
 fun auto_fixes (arg as (ctxt, (propss, x))) =
-  if Variable.is_body ctxt then arg
-  else ((fold o fold) Variable.fix_frees propss ctxt, (propss, x));
+  ((fold o fold) Variable.auto_fixes propss ctxt, (propss, x));
 
 fun bind_fixes xs ctxt =
   let
diff -r 6cca4865e388 -r d9dd7b4e5e69 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:00 2006 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Nov 14 22:17:01 2006 +0100
@@ -86,6 +86,7 @@
 
 fun read_specification x =
   prep_specification ProofContext.read_vars ProofContext.read_propp Attrib.intern_src x;
+
 fun cert_specification x =
   prep_specification ProofContext.cert_vars ProofContext.cert_propp (K I) x;
 
@@ -100,7 +101,7 @@
 
     val ((consts, axioms), lthy') = lthy
       |> LocalTheory.consts spec_frees vars
-      ||> fold (fold Variable.fix_frees o snd) specs   (* FIXME !? *)
+      ||> fold (fold Variable.auto_fixes o snd) specs   (* FIXME !? *)
       ||>> LocalTheory.axioms specs;
 
     (* FIXME generic target!? *)
@@ -206,7 +207,7 @@
     Element.Shows shows =>
       let
         val (_, _, elems_ctxt, propp) = prep_stmt elems (map snd shows) ctxt;
-        val goal_ctxt = fold (fold (Variable.fix_frees o fst)) propp elems_ctxt;
+        val goal_ctxt = fold (fold (Variable.auto_fixes o fst)) propp elems_ctxt;
         val stmt = Attrib.map_specs prep_att (map fst shows ~~ propp);
       in ((stmt, []), goal_ctxt) end
   | Element.Obtains obtains =>
@@ -232,7 +233,7 @@
             val asm = Term.list_all_free (parms, Logic.list_implies (props, thesis));
           in
             ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
-            ctxt' |> Variable.fix_frees asm
+            ctxt' |> Variable.auto_fixes asm
             |> ProofContext.add_assms_i Assumption.assume_export
               [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)