--- a/TFL/rules.ML Thu Jul 27 23:28:27 2006 +0200
+++ b/TFL/rules.ML Thu Jul 27 23:28:28 2006 +0200
@@ -816,7 +816,7 @@
fun prove strict (ptm, tac) =
let
val {thy, t, ...} = Thm.rep_cterm ptm;
- val ctxt = ProofContext.init thy |> ProofContext.fix_frees t;
+ val ctxt = ProofContext.init thy |> Variable.fix_frees t;
in
if strict then Goal.prove ctxt [] [] t (K tac)
else Goal.prove ctxt [] [] t (K tac)
--- a/src/Pure/Isar/local_theory.ML Thu Jul 27 23:28:27 2006 +0200
+++ b/src/Pure/Isar/local_theory.ML Thu Jul 27 23:28:28 2006 +0200
@@ -249,7 +249,7 @@
in
fun axioms_finish finish = fold_map (fn ((name, atts), props) =>
- fold ProofContext.fix_frees props
+ fold Variable.fix_frees props
#> (fn ctxt => ctxt
|> theory_result (fold_map (add_axiom (hyps_of ctxt)) (PureThy.name_multi name props))
|-> (fn ths => note ((name, atts), map (finish ctxt) ths))));
--- a/src/Pure/Isar/locale.ML Thu Jul 27 23:28:27 2006 +0200
+++ b/src/Pure/Isar/locale.ML Thu Jul 27 23:28:28 2006 +0200
@@ -882,7 +882,7 @@
val ts = maps (map #1 o #2) asms';
val (ps, qs) = chop (length ts) axs;
val (_, ctxt') =
- ctxt |> fold ProofContext.fix_frees ts
+ ctxt |> fold Variable.fix_frees 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) =
@@ -894,7 +894,7 @@
let val ((c, _), t') = LocalDefs.cert_def ctxt t
in (t', ((if name = "" then Thm.def_name c else name, atts), [(t', ps)])) end);
val (_, ctxt') =
- ctxt |> fold (ProofContext.fix_frees o #1) asms
+ ctxt |> fold (Variable.fix_frees 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) =