# HG changeset patch
# User blanchet
# Date 1272380739 -7200
# Node ID 1e01a7162435b6dc383f42f439d08c1801c80eb5
# Parent  fcbf412c560f6025bc2184697cfebf22323019cf
polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs

diff -r fcbf412c560f -r 1e01a7162435 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 16:12:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 17:05:39 2010 +0200
@@ -492,9 +492,9 @@
 
 fun add_fact_from_dep thm_names num =
   if is_axiom_clause_number thm_names num then
-    apsnd (cons (Vector.sub (thm_names, num - 1)))
+    apsnd (insert (op =) (Vector.sub (thm_names, num - 1)))
   else
-    apfst (cons (raw_prefix, num))
+    apfst (insert (op =) (raw_prefix, num))
 
 fun generalize_all_vars t = fold_rev Logic.all (map Var (Term.add_vars t [])) t
 fun step_for_tuple _ _ (label, t, []) = Assume ((raw_prefix, label), t)
@@ -809,11 +809,13 @@
         suffix ^ "\n"
       end
     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
-    and do_proof proof =
-      (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
-      do_indent 0 ^ "proof -\n" ^
-      do_steps "" "" 1 proof ^
-      do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
+    (* One-step proofs are pointless; better use the Metis one-liner. *)
+    and do_proof [_] = ""
+      | do_proof proof =
+        (if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
+        do_indent 0 ^ "proof -\n" ^
+        do_steps "" "" 1 proof ^
+        do_indent 0 ^ (if n <> 1 then "next" else "qed") ^ "\n"
   in setmp_CRITICAL show_sorts sorts do_proof end
 
 fun isar_proof_text (pool, debug, shrink_factor, sorts, ctxt, conjecture_shape)