# HG changeset patch
# User blanchet
# Date 1351679001 -3600
# Node ID e12b4e9794fdb4633f633a0bf77e851e14ac6a10
# Parent  34b0464d7eef48620709c5090ce937829bee30fb
tuning

diff -r 34b0464d7eef -r e12b4e9794fd src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -232,8 +232,9 @@
   end
 
 fun hackish_string_for_term thy t =
-  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
-                   (print_mode_value ())) (Syntax.string_of_term_global thy) t
+  Print_Mode.setmp
+    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
+    (Syntax.string_of_term_global thy) t
   |> String.translate (fn c => if Char.isPrint c then str c else "")
   |> simplify_spaces
 
@@ -241,9 +242,8 @@
    they are displayed as "M" and we want to avoid clashes with these. But
    sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
    prefixes of all free variables. In the worse case scenario, where the fact
-   won't be resolved correctly, the user can fix it manually, e.g., by naming
-   the fact in question. Ideally we would need nothing of it, but backticks
-   simply don't work with schematic variables. *)
+   won't be resolved correctly, the user can fix it manually, e.g., by giving a
+   name to the offending fact. *)
 fun all_prefixes_of s =
   map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
 
diff -r 34b0464d7eef -r e12b4e9794fd src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Oct 31 11:23:21 2012 +0100
@@ -86,7 +86,7 @@
   in
     Source.of_string name
     |> Symbol.source
-    |> Token.source {do_recover=SOME false} lex Position.start
+    |> Token.source {do_recover = SOME false} lex Position.start
     |> Token.source_proper
     |> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE
     |> Source.exhaust