# HG changeset patch
# User blanchet
# Date 1272560856 -7200
# Node ID f1cb249f6384f1dd07a94ddd50fa866a5961ab89
# Parent  f91342f218a9c9652dbe13b0a66b5800dbea3393
uncomment code

diff -r f91342f218a9 -r f1cb249f6384 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 19:02:04 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Apr 29 19:07:36 2010 +0200
@@ -642,11 +642,9 @@
       |> parse_proof pool
       |> decode_lines ctxt
       |> rpair [] |-> fold_rev (add_line conjecture_shape thm_names)
-(*###
       |> rpair [] |-> fold_rev add_nontrivial_line
       |> rpair (0, []) |-> fold_rev (add_desired_line ctxt shrink_factor frees)
       |> snd
-*)
   in
     (if null frees then [] else [Fix frees]) @
     map2 (step_for_line thm_names) (length lines downto 1) lines