--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 21:31:25 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Feb 14 22:49:22 2013 +0100
@@ -22,7 +22,8 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts
+ Case_Split of isar_step list list * facts |
+ Subblock of isar_step list
val string_for_label : label -> string
val metis_steps_top_level : isar_step list -> int
@@ -45,7 +46,8 @@
Prove of isar_qualifier list * label * term * byline
and byline =
By_Metis of facts |
- Case_Split of isar_step list list * facts
+ Case_Split of isar_step list list * facts |
+ Subblock of isar_step list
fun string_for_label (s, num) = s ^ string_of_int num
@@ -57,6 +59,8 @@
| Prove (_, _, _, By_Metis _) => Integer.add 1
| Prove (_, _, _, Case_Split (cases, _)) =>
Integer.add (fold (Integer.add o metis_steps_total) cases 1)
+ | Prove (_, _, _, Subblock subproof) =>
+ Integer.add (metis_steps_total subproof)
| _ => I) proof 0
end