# HG changeset patch
# User blanchet
# Date 1412015164 -7200
# Node ID b4c0e2b00036f451219e21d22a78fbc4948f6ce9
# Parent  7836013951e6d9497608decc80952498c8cbebf7
support hypotheses with schematics in Isar proofs

diff -r 7836013951e6 -r b4c0e2b00036 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 29 18:37:33 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Sep 29 20:26:04 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 7836013951e6 -r b4c0e2b00036 src/HOL/Tools/SMT/smtlib_isar.ML
--- a/src/HOL/Tools/SMT/smtlib_isar.ML	Mon Sep 29 18:37:33 2014 +0200
+++ b/src/HOL/Tools/SMT/smtlib_isar.ML	Mon Sep 29 20:26:04 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;