src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 49981 e12b4e9794fd
parent 48667 ac58317ef11f
child 50047 45684acf0b94
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 31 11:23:21 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Oct 31 11:23:21 2012 +0100
     1.3 @@ -232,8 +232,9 @@
     1.4    end
     1.5  
     1.6  fun hackish_string_for_term thy t =
     1.7 -  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
     1.8 -                   (print_mode_value ())) (Syntax.string_of_term_global thy) t
     1.9 +  Print_Mode.setmp
    1.10 +    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
    1.11 +    (Syntax.string_of_term_global thy) t
    1.12    |> String.translate (fn c => if Char.isPrint c then str c else "")
    1.13    |> simplify_spaces
    1.14  
    1.15 @@ -241,9 +242,8 @@
    1.16     they are displayed as "M" and we want to avoid clashes with these. But
    1.17     sometimes it's even worse: "Ma__" encodes "M". So we simply reserve all
    1.18     prefixes of all free variables. In the worse case scenario, where the fact
    1.19 -   won't be resolved correctly, the user can fix it manually, e.g., by naming
    1.20 -   the fact in question. Ideally we would need nothing of it, but backticks
    1.21 -   simply don't work with schematic variables. *)
    1.22 +   won't be resolved correctly, the user can fix it manually, e.g., by giving a
    1.23 +   name to the offending fact. *)
    1.24  fun all_prefixes_of s =
    1.25    map (fn i => String.extract (s, 0, SOME i)) (1 upto size s - 1)
    1.26