# HG changeset patch
# User blanchet
# Date 1272377571 -7200
# Node ID fcbf412c560f6025bc2184697cfebf22323019cf
# Parent  1aba777a367f6eb08c92721b7900fc3b4cac39fb
reintroduce missing "gen_all_vars" call

diff -r 1aba777a367f -r fcbf412c560f src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:00:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:12:51 2010 +0200
@@ -331,8 +331,6 @@
                                                    ctxt)
   end
 
-fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
-
 fun decode_line vt0 (name, ts, deps) ctxt =
   let val cl = clause_of_strees ctxt vt0 ts in
     ((name, cl, deps), fold Variable.declare_term (OldTerm.term_frees cl) ctxt)
@@ -498,9 +496,11 @@
   else
     apfst (cons (raw_prefix, num))
 
+fun generalize_all_vars t = fold_rev Logic.all (map Var (Term.add_vars t [])) t
 fun step_for_tuple _ _ (label, t, []) = Assume ((raw_prefix, label), t)
   | step_for_tuple thm_names j (label, t, deps) =
-    Have (if j = 1 then [Show] else [], (raw_prefix, label), t,
+    Have (if j = 1 then [Show] else [], (raw_prefix, label),
+          generalize_all_vars (HOLogic.mk_Trueprop t),
           Facts (fold (add_fact_from_dep thm_names) deps ([], [])))
 
 fun strip_spaces_in_list [] = ""
@@ -795,11 +795,11 @@
         do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n"
       | do_step ind (Have (qs, l, t, Facts facts)) =
         do_indent ind ^ do_have qs ^ " " ^
-        do_label l ^ do_term t ^ do_facts facts ^ "\n"
+        do_label l ^ do_term t ^ " " ^ do_facts facts ^ "\n"
       | do_step ind (Have (qs, l, t, CaseSplit (proofs, facts))) =
         space_implode (do_indent ind ^ "moreover\n")
                       (map (do_block ind) proofs) ^
-        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^
+        do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ " " ^
         do_facts facts ^ "\n"
     and do_steps prefix suffix ind steps =
       let val s = implode (map (do_step ind) steps) in