# HG changeset patch
# User wenzelm
# Date 1138559031 -3600
# Node ID 9dd7898410184fab8894b6fd22c5b216db6faa4b
# Parent  23db974a0575220a6cb13f613aca92b4d2884216
invent_fixes: merely enter body temporarily;

diff -r 23db974a0575 -r 9dd789841018 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Jan 29 19:23:50 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Jan 29 19:23:51 2006 +0100
@@ -1108,7 +1108,7 @@
 fun no_dups _ [] = ()
   | no_dups ctxt dups = error ("Duplicate variable(s): " ^ commas_quote dups);
 
-fun gen_fixes prep invent raw_vars ctxt =
+fun gen_fixes prep raw_vars ctxt =
   let
     val (ys, zs) = split_list (fixes_of ctxt);
     val (vars, ctxt') = prep raw_vars ctxt;
@@ -1116,7 +1116,6 @@
     val _ = no_dups ctxt (duplicates xs);
     val xs' =
       if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
-      else if invent then Term.variantlist (xs, zs)
       else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);
     val vars' = map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars;
   in
@@ -1129,14 +1128,22 @@
 
 in
 
-val add_fixes = gen_fixes read_vars false;
-val add_fixes_i = gen_fixes cert_vars false;
-val add_fixes_legacy = gen_fixes cert_vars_legacy false;
-fun invent_fixes xs = gen_fixes cert_vars true (map (fn x => (x, NONE, NoSyn)) xs);
+val add_fixes = gen_fixes read_vars;
+val add_fixes_i = gen_fixes cert_vars;
+val add_fixes_legacy = gen_fixes cert_vars_legacy;
 
 end;
 
 
+(* invent fixes *)
+
+fun invent_fixes xs ctxt =
+  ctxt
+  |> set_body true
+  |> add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs)
+  ||> restore_body ctxt;
+
+
 (* fixes vs. frees *)
 
 fun fix_frees t ctxt =