# HG changeset patch
# User blanchet
# Date 1272555586 -7200
# Node ID bba1e5f2b643ef29c87f65c9041d07c2ebef3a92
# Parent  c6c2661bf08ede50926854050e69819ecadbc0bd
one-step Isar proofs are not always pointless

diff -r c6c2661bf08e -r bba1e5f2b643 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 17:31:08 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 17:39:46 2010 +0200
@@ -924,9 +924,7 @@
         suffix ^ "\n"
       end
     and do_block ind proof = do_steps "{ " " }" (ind + 1) proof
-    (* One-step proofs are pointless; better use the Metis one-liner. *)
-    and do_proof [_] = ""
-      | do_proof 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 ^