# HG changeset patch
# User wenzelm
# Date 1154035705 -7200
# Node ID a7b027328d6e8e7595a461a3a2f55cafc459afc0
# Parent  620a3f2970720a0fa7be49d25938faba06c5f235
added fix_frees (from Isar/proof_context.ML);

diff -r 620a3f297072 -r a7b027328d6e src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Jul 27 23:28:23 2006 +0200
+++ b/src/Pure/variable.ML	Thu Jul 27 23:28:25 2006 +0200
@@ -27,6 +27,7 @@
   val thm_context: thm -> Context.proof
   val variant_frees: Context.proof -> term list -> (string * 'a) list -> (string * 'a) list
   val add_fixes: string list -> Context.proof -> string list * Context.proof
+  val fix_frees: term -> Context.proof -> Context.proof
   val invent_fixes: string list -> Context.proof -> string list * Context.proof
   val invent_types: sort list -> Context.proof -> (string * sort) list * Context.proof
   val export_inst: Context.proof -> Context.proof -> string list * string list
@@ -234,6 +235,18 @@
         (xs, fold Name.declare xs names));
   in ctxt |> new_fixes names' xs xs' end;
 
+fun fix_frees t ctxt =
+  let
+    val fixes = rev (fold_aterms (fn Free (x, _) =>
+      if is_fixed ctxt x then I else insert (op =) x | _ => I) t []);
+  in
+    ctxt
+    |> set_body false
+    |> (snd o add_fixes fixes)
+    |> restore_body ctxt
+    |> declare_term t
+  end;
+
 fun invent_fixes raw_xs ctxt =
   let
     val names = names_of ctxt;