src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML

     Obtain of
       isar_qualifier list * (string * typ) list * label * term * byline |
     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
   val metis_steps_total : isar_step list -> int
 end

   Assume of label * term |
   Obtain of isar_qualifier list * (string * typ) list * label * term * byline |
   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
 
 fun metis_steps_top_level proof =
   fold (fn Obtain _ => Integer.add 1 | Prove _ => Integer.add 1 | _ => I)

 fun metis_steps_total proof =
   fold (fn Obtain _ => Integer.add 1
          | 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