--- 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;