# HG changeset patch
# User blanchet
# Date 1272202233 -7200
# Node ID 417cdfb2746a0c2ddf360b9753727533b5fddf5e
# Parent  e73923451f6f89d2281d1036a476b89235337361
cosmetics

diff -r e73923451f6f -r 417cdfb2746a src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Apr 25 15:04:20 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Sun Apr 25 15:30:33 2010 +0200
@@ -411,20 +411,20 @@
                               (print_mode_value ()))
                       (Syntax.string_of_term ctxt)
     fun have_or_show "show" _ = "  show \""
-      | have_or_show have lname = "  " ^ have ^ " " ^ lname ^ ": \""
-    fun do_line _ (lname, t, []) =
+      | have_or_show have label = "  " ^ have ^ " " ^ label ^ ": \""
+    fun do_line _ (label, t, []) =
        (* No depedencies: it's a conjecture clause, with no proof. *)
        (case permuted_clause t ctms of
-          SOME u => "  assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+          SOME u => "  assume " ^ label ^ ": \"" ^ string_of_term u ^ "\"\n"
         | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
                               [t]))
-      | do_line have (lname, t, deps) =
-        have_or_show have lname ^
+      | do_line have (label, t, deps) =
+        have_or_show have label ^
         string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
         "\"\n    by (metis " ^ space_implode " " deps ^ ")\n"
-    fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
-      | do_lines ((lname, t, deps) :: lines) =
-        do_line "have" (lname, t, deps) :: do_lines lines
+    fun do_lines [(label, t, deps)] = [do_line "show" (label, t, deps)]
+      | do_lines ((label, t, deps) :: lines) =
+        do_line "have" (label, t, deps) :: do_lines lines
   in setmp_CRITICAL show_sorts sorts do_lines end;
 
 fun unequal t (_, t', _) = not (t aconv t');
@@ -497,13 +497,15 @@
       stringify_deps thm_names deps_map lines
     else
       let
-        val lname = Int.toString (length deps_map)
-        fun fix num = if is_axiom_clause_number thm_names num
-                      then SOME(Vector.sub(thm_names,num-1))
-                      else AList.lookup (op =) deps_map num;
+        val label = Int.toString (length deps_map)
+        fun string_for_num num =
+          if is_axiom_clause_number thm_names num then
+            SOME (Vector.sub (thm_names, num - 1))
+          else
+            AList.lookup (op =) deps_map num
       in
-        (lname, t, map_filter fix (distinct (op=) deps)) ::
-        stringify_deps thm_names ((num, lname) :: deps_map) lines
+        (label, t, map_filter string_for_num (distinct (op=) deps)) ::
+        stringify_deps thm_names ((num, label) :: deps_map) lines
       end
 
 fun isar_proof_start i =