--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML Sun Feb 02 20:53:51 2014 +0100
@@ -40,7 +40,7 @@
val string_of_proof_method : proof_method -> string
- val steps_of_proof : isar_proof -> isar_step list
+ val steps_of_isar_proof : isar_proof -> isar_step list
val label_of_isar_step : isar_step -> label option
val byline_of_isar_step : isar_step -> (facts * proof_method list) option
@@ -119,7 +119,7 @@
| Meson_Method => "meson"
| Algebra_Method => "algebra")
-fun steps_of_proof (Proof (_, _, steps)) = steps
+fun steps_of_isar_proof (Proof (_, _, steps)) = steps
fun label_of_isar_step (Prove (_, _, l, _, _, _)) = SOME l
| label_of_isar_step _ = NONE
@@ -131,7 +131,7 @@
| byline_of_isar_step _ = NONE
fun fold_isar_step f step =
- fold (steps_of_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
+ fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
and fold_isar_steps f = fold (fold_isar_step f)
fun map_isar_steps f =
@@ -170,7 +170,7 @@
let
val used_ls =
fold_isar_steps (byline_of_isar_step #> (fn SOME ((ls, _), _) => union (op =) ls | _ => I))
- (steps_of_proof proof) []
+ (steps_of_isar_proof proof) []
fun kill_label l = if member (op =) used_ls l then l else no_label