# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 7f2930d9bb2c4d3e6d8182340b2421405afae612
# Parent  8cc42c1f9bb53039dfcf207f73aaa8a354c9534d
tuning

diff -r 8cc42c1f9bb5 -r 7f2930d9bb2c src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -51,43 +51,40 @@
 
 fun postprocess_isar_proof_remove_unreferenced_steps postproc_step =
   let
-    val add_lfs = fold (Ord_List.insert label_ord)
-
-    fun do_proof (Proof (fix, assms, steps)) =
-      let val (refed, steps) = do_steps steps in
+    fun process_proof (Proof (fix, assms, steps)) =
+      let val (refed, steps) = process_steps steps in
         (refed, Proof (fix, assms, steps))
       end
-    and do_steps [] = ([], [])
-      | do_steps steps =
+    and process_steps [] = ([], [])
+      | process_steps steps =
         (* the last step is always implicitly referenced *)
-        let val (steps, (refed, concl)) = split_last steps ||> do_refed_step in
-          fold_rev do_step steps (refed, [concl])
+        let val (steps, (refed, concl)) = split_last steps ||> process_referenced_step in
+          fold_rev process_step steps (refed, [concl])
         end
-    and do_step step (refed, accu) =
+    and process_step step (refed, accu) =
       (case label_of_isar_step step of
         NONE => (refed, step :: accu)
       | SOME l =>
         if Ord_List.member label_ord refed l then
-          do_refed_step step
+          process_referenced_step step
           |>> Ord_List.union label_ord refed
           ||> (fn x => x :: accu)
         else
           (refed, accu))
-    and do_refed_step step = step |> postproc_step |> do_refed_step'
-    and do_refed_step' (Let _) = raise Fail "Sledgehammer_Isar_Minimize"
-      | do_refed_step' (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))) =
-        let
-          val (refed, subproofs) =
-            map do_proof subproofs
-            |> split_list
-            |>> Ord_List.unions label_ord
-            |>> add_lfs lfs
-          val step = Prove (qs, xs, l, t, subproofs, ((lfs, gfs), m))
-        in
-          (refed, step)
-        end
+    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))) =
+      let
+        val (refed, 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))
+      in
+        (refed, step)
+      end
   in
-    snd o do_proof
+    snd o process_proof
   end
 
 end;