src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50048 fb024bbf4b65
parent 50047 45684acf0b94
child 50049 dd6a4655cd72
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:32:22 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Nov 12 11:52:37 2012 +0100
     1.3 @@ -231,12 +231,8 @@
     1.4      exists_low_level_class_const t orelse is_that_fact th
     1.5    end
     1.6  
     1.7 -fun hackish_string_for_term ctxt t =
     1.8 -  Print_Mode.setmp
     1.9 -    (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ()))
    1.10 -    (Syntax.string_of_term ctxt) t
    1.11 -  |> String.translate (fn c => if Char.isPrint c then str c else "")
    1.12 -  |> simplify_spaces
    1.13 +fun hackish_string_for_term ctxt =
    1.14 +  with_vanilla_print_mode (Syntax.string_of_term ctxt) #> repair_printed_term
    1.15  
    1.16  (* This is a terrible hack. Free variables are sometimes coded as "M__" when
    1.17     they are displayed as "M" and we want to avoid clashes with these. But