Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
uncomment code
authorblanchet
Thu, 29 Apr 2010 19:07:36 +0200
changeset 36567 f1cb249f6384
parent 36566 f91342f218a9
child 36568 d495d2e1f0a6
uncomment code
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle