# HG changeset patch
# User blanchet
# Date 1391099682 -3600
# Node ID fafdf2424c57abdc2dadad8ca4362632e030c6c9
# Parent  a0bd8d6414e69ab8ef44a9d2d358caa89f1f92c7
don't forget the last inference(s) after conjecture skolemization

diff -r a0bd8d6414e6 -r fafdf2424c57 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 16:40:31 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Jan 30 17:34:42 2014 +0100
@@ -329,7 +329,7 @@
                   [g] =>
                   if skolem andalso is_clause_tainted g then
                     let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
-                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] []
+                      isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methodss)] infs
                     end
                   else
                     do_rest l (prove [] by)
@@ -339,8 +339,8 @@
             end
           | isar_steps outer predecessor accum (Cases cases :: infs) =
             let
-              fun isar_case (c, infs) =
-                isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] infs
+              fun isar_case (c, subinfs) =
+                isar_proof false [] [(label_of_clause c, prop_of_clause c)] [] subinfs
               val c = succedent_of_cases cases
               val l = label_of_clause c
               val t = prop_of_clause c