# 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)