# HG changeset patch
# User blanchet
# Date 1412019602 -7200
# Node ID f4a63cb6a58aa94e1ed31c169702df279a6efd52
# Parent  b4c0e2b00036f451219e21d22a78fbc4948f6ce9# Parent  d5f24630c10454810bd7dcfd81c00ece75b667cc
merge

diff -r d5f24630c104 -r f4a63cb6a58a src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 29 21:34:48 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 29 21:40:02 2014 +0200
@@ -757,7 +757,8 @@
         val (ss', role', t') =
           (case resolve_conjectures ss of
             [j] =>
-            if j = length hyp_ts then ([], Conjecture, concl_t) else ([], Hypothesis, nth hyp_ts j)
+            if j = length hyp_ts then ([], Conjecture, concl_t)
+            else ([], Hypothesis, close_form (nth hyp_ts j))
           | _ =>
             (case resolve_facts facts ss of
               [] => (ss, if role = Lemma then Lemma else Plain, t)
diff -r d5f24630c104 -r f4a63cb6a58a src/HOL/Tools/SMT/smtlib_isar.ML
--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Mon Sep 29 21:34:48 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Mon Sep 29 21:40:02 2014 +0200
@@ -11,7 +11,7 @@
   val postprocess_step_conclusion: Proof.context -> thm list -> term list -> term -> term
   val normalizing_prems : Proof.context -> term -> (string * string list) list
   val distinguish_conjecture_and_hypothesis : ''a list -> ''b -> ''b -> ''b list ->
-    (''a * 'c) list -> 'c list -> 'c -> (ATP_Problem.atp_formula_role * 'c) option
+    (''a * term) list -> term list -> term -> (ATP_Problem.atp_formula_role * term) option
   val unskolemize_names: Proof.context -> term -> term
 end;
 
@@ -70,6 +70,6 @@
     else
      (case find_index (curry (op =) id) prem_ids of
        ~1 => NONE (* lambda-lifting definition *)
-     | i => SOME (Hypothesis, nth hyp_ts i)))
+     | i => SOME (Hypothesis, close_form (nth hyp_ts i))))
 
 end;