# HG changeset patch
# User blanchet
# Date 1391418858 -3600
# Node ID bd9f033b9896073d397484886390f9f20297aba3
# Parent  43473497fb65557cf6eba1466c4407b6329bbc6f
tuning

diff -r 43473497fb65 -r bd9f033b9896 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -55,36 +55,32 @@
 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
   let
     fun process_proof (Proof (fix, assms, steps)) =
-      let val (refed, steps) = process_steps steps in
-        (refed, Proof (fix, assms, steps))
-      end
+      process_steps steps ||> (fn steps => Proof (fix, assms, steps))
     and process_steps [] = ([], [])
       | process_steps steps =
         (* the last step is always implicitly referenced *)
-        let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in
-          fold_rev process_step steps (refed, [concl])
+        let val (steps, (used, concl)) = split_last steps ||> process_used_step in
+          fold_rev process_step steps (used, [concl])
         end
-    and process_step step (refed, accu) =
+    and process_step step (used, accu) =
       (case label_of_isar_step step of
-        NONE => (refed, step :: accu)
+        NONE => (used, step :: accu)
       | SOME l =>
-        if Ord_List.member label_ord refed l then
-          process_referenced_step step
-          |>> Ord_List.union label_ord refed
-          ||> (fn x => x :: accu)
+        if Ord_List.member label_ord used l then
+          process_used_step step |>> Ord_List.union label_ord used ||> (fn step => step :: accu)
         else
-          (refed, accu))
-    and process_referenced_step step = step |> postproc_step |> process_referenced_step_subproofs
-    and process_referenced_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
+          (used, accu))
+    and process_used_step step = step |> postproc_step |> process_used_step_subproofs
+    and process_used_step_subproofs (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
       let
-        val (refed, subproofs) =
+        val (used, subproofs) =
           map process_proof subproofs
           |> split_list
           |>> Ord_List.unions label_ord
           |>> fold (Ord_List.insert label_ord) lfs
-        val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
+        val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))
       in
-        (refed, step)
+        (used, step)
       end
   in
     snd o process_proof