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.
make compile (and not just load dynamically)
authorblanchet
Mon, 26 Apr 2010 21:41:54 +0200
changeset 36404 cb3dc64f13d7
parent 36403 9a4baad039c4
child 36405 05a8d79eb338
make compile (and not just load dynamically)
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 26 21:25:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Mon Apr 26 21:41:54 2010 +0200
@@ -799,10 +799,9 @@
        else
          if member (op =) qs Show then "show" else "have")
     val do_term =
-      Nitpick_Util.maybe_quote
-      o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                                (print_mode_value ()))
-                        (Syntax.string_of_term ctxt)
+      quote o PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+                                      (print_mode_value ()))
+                              (Syntax.string_of_term ctxt)
     fun do_using [] = ""
       | do_using ls = "using " ^ (space_implode " " (map do_raw_label ls)) ^ " "
     fun do_by_facts [] [] = "by blast"
isabelle