# HG changeset patch
# User blanchet
# Date 1272310914 -7200
# Node ID cb3dc64f13d7506a395b431c3b7754b235ec59c1
# Parent  9a4baad039c4285ed300968fd74f6b2bb515af8a
make compile (and not just load dynamically)

diff -r 9a4baad039c4 -r cb3dc64f13d7 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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"