--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Mon Dec 16 12:26:18 2013 +0100
@@ -18,7 +18,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method)
+ (facts * proof_method list)
and proof_method =
Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
Blast_Method | Meson_Method
@@ -38,8 +38,7 @@
val label_of_step : isar_step -> label option
val subproofs_of_step : isar_step -> isar_proof list option
- val byline_of_step : isar_step -> (facts * proof_method) option
- val proof_method_of_step : isar_step -> proof_method option
+ val byline_of_step : isar_step -> (facts * proof_method list) option
val use_metis_new_skolem : isar_step -> bool
val fold_isar_step : (isar_step -> 'a -> 'a) -> isar_step -> 'a -> 'a
@@ -69,7 +68,7 @@
and isar_step =
Let of term * term |
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
- (facts * proof_method)
+ (facts * proof_method list)
and proof_method =
Metis_Method | Simp_Method | Auto_Method | Fastforce_Method | Force_Method | Arith_Method |
Blast_Method | Meson_Method
@@ -96,12 +95,9 @@
fun byline_of_step (Prove (_, _, _, _, _, byline)) = SOME byline
| byline_of_step _ = NONE
-fun proof_method_of_step (Prove (_, _, _, _, _, (_, method))) = SOME method
- | proof_method_of_step _ = NONE
-
(* The new skolemizer puts the arguments in the same order as the ATPs (E and Vampire -- but see
also "atp_proof_reconstruct.ML" concerning Vampire). *)
-fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth))) =
+fun use_metis_new_skolem (Prove (_, xs, _, _, _, (_, meth :: _))) =
meth = Metis_Method andalso exists (fn (_, T) => length (binder_types T) > 1) xs
| use_metis_new_skolem _ = false