tuned data structure

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -230,9 +230,9 @@
               val skolem = is_skolemize_rule rule
 
               fun prove sub by = Prove (maybe_show outer c [], [], l, t, sub, by)
-              fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
+              fun steps_of_rest l step = isar_steps outer (SOME l) (step :: accum) infs
 
-              val deps = fold add_fact_of_dependencies gamma no_facts
+              val deps = fold add_fact_of_dependencies gamma ([], [])
               val meths =
                 (if skolem then skolem_methods
                  else if is_arith_rule rule then arith_methods
@@ -246,13 +246,14 @@
                   [g] =>
                   if skolem andalso is_clause_tainted g then
                     let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
-                      isar_steps outer (SOME l) [prove [subproof] (no_facts, meths)] infs
+                      isar_steps outer (SOME l) [prove [subproof] (([], []), meths)] infs
                     end
                   else
-                    do_rest l (prove [] by)
-                | _ => do_rest l (prove [] by))
+                    steps_of_rest l (prove [] by)
+                | _ => steps_of_rest l (prove [] by))
               else
-                do_rest l (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
+                steps_of_rest l
+                  (if skolem then Prove ([], skolems_of t, l, t, [], by) else prove [] by)
             end
           | isar_steps outer predecessor accum (Cases cases :: infs) =
             let

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -169,7 +169,7 @@
         outcome as Played _ => SOME (meth, outcome)
       | _ => NONE)
 
-    val meths = snd (byline_of_isar_step step)
+    val meths = proof_methods_of_isar_step step
   in
     the_list (Par_List.get_some try_method meths)
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:30:53 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 11:37:48 2014 +0100
@@ -33,7 +33,6 @@
       (facts * proof_method list)
 
   val no_label : label
-  val no_facts : facts
 
   val label_ord : label * label -> order
   val string_of_label : label -> string
@@ -43,7 +42,8 @@
   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
+  val facts_of_isar_step : isar_step -> facts
+  val proof_methods_of_isar_step : isar_step -> proof_method list
 
   val fold_isar_steps : (isar_step -> 'a -> 'a) -> isar_step list -> 'a -> 'a
   val map_isar_steps : (isar_step -> isar_step) -> isar_proof -> isar_proof
@@ -98,7 +98,6 @@
     (facts * proof_method list)
 
 val no_label = ("", ~1)
-val no_facts = ([],[])
 
 val label_ord = pairself swap #> prod_ord int_ord fast_string_ord
 
@@ -127,8 +126,11 @@
 fun subproofs_of_isar_step (Prove (_, _, _, _, subproofs, _)) = SOME subproofs
   | subproofs_of_isar_step _ = NONE
 
-fun byline_of_isar_step (Prove (_, _, _, _, _, byline)) = byline
-  | byline_of_isar_step _ = (([], []), [])
+fun facts_of_isar_step (Prove (_, _, _, _, _, (facts, _))) = facts
+  | facts_of_isar_step _ = ([], [])
+
+fun proof_methods_of_isar_step (Prove (_, _, _, _, _, (_, meths))) = meths
+  | proof_methods_of_isar_step _ = []
 
 fun fold_isar_step f step =
   fold (steps_of_isar_proof #> fold_isar_steps f) (these (subproofs_of_isar_step step)) #> f step
@@ -169,8 +171,7 @@
 fun kill_useless_labels_in_isar_proof proof =
   let
     val used_ls =
-      fold_isar_steps (byline_of_isar_step #> (fn ((ls, _), _) => union (op =) ls | _ => I))
-        (steps_of_isar_proof proof) []
+      fold_isar_steps (facts_of_isar_step #> fst #> union (op =)) (steps_of_isar_proof proof) []
 
     fun kill_label l = if member (op =) used_ls l then l else no_label
 
@@ -188,34 +189,34 @@
     fun next_label l (next, subst) =
       let val l' = ("", next) in (l', (next + 1, (l, l') :: subst)) end
 
-    fun do_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
+    fun relabel_byline by (_, subst) = apfst (apfst (map (AList.lookup (op =) subst #> the))) by
     handle Option.Option =>
       raise Fail "Sledgehammer_Isar_Proof: relabel_isar_proof_canonically"
 
-    fun do_assm (l, t) state =
+    fun relabel_assm (l, t) state =
       let
         val (l, state) = next_label l state
       in ((l, t), state) end
 
-    fun do_proof (Proof (fix, assms, steps)) state =
+    fun relabel_proof (Proof (fix, assms, steps)) state =
       let
-        val (assms, state) = fold_map do_assm assms state
-        val (steps, state) = fold_map do_step steps state
+        val (assms, state) = fold_map relabel_assm assms state
+        val (steps, state) = fold_map relabel_step steps state
       in
         (Proof (fix, assms, steps), state)
       end
 
-    and do_step (step as Let _) state = (step, state)
-      | do_step (Prove (qs, fix, l, t, subproofs, by)) state=
+    and relabel_step (step as Let _) state = (step, state)
+      | relabel_step (Prove (qs, fix, l, t, subproofs, by)) state=
         let
-          val by = do_byline by state
-          val (subproofs, state) = fold_map do_proof subproofs state
+          val by = relabel_byline by state
+          val (subproofs, state) = fold_map relabel_proof subproofs state
           val (l, state) = next_label l state
         in
           (Prove (qs, fix, l, t, subproofs, by), state)
         end
   in
-    fst (do_proof proof (0, []))
+    fst (relabel_proof proof (0, []))
   end
 
 val assume_prefix = "a"