# HG changeset patch
# User wenzelm
# Date 1154127093 -7200
# Node ID 6379135f21c2cfe3dcc152aabe226aa5cdb62d52
# Parent  c3f2097527492c1ce5e0207470b07d7b76ebbbb5
added add_fixes_direct;
tuned;

diff -r c3f209752749 -r 6379135f21c2 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sat Jul 29 00:51:32 2006 +0200
+++ b/src/Pure/variable.ML	Sat Jul 29 00:51:33 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 add_fixes_direct: string list -> Context.proof -> 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
@@ -235,18 +236,6 @@
         (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;
@@ -256,6 +245,18 @@
 
 end;
 
+
+fun add_fixes_direct xs ctxt = ctxt
+  |> set_body false
+  |> (snd o add_fixes xs)
+  |> restore_body ctxt;
+
+fun fix_frees t ctxt = ctxt
+  |> add_fixes_direct
+      (rev (fold_aterms (fn Free (x, _) =>
+        if is_fixed ctxt x then I else insert (op =) x | _ => I) t []))
+  |> declare_term t;
+
 fun invent_types Ss ctxt =
   let
     val tfrees = Name.invents (names_of ctxt) "'a" (length Ss) ~~ Ss;