src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 66020 a31760eee09d
parent 64573 e6aee01da22d
child 67498 88a02f41246a
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Jun 05 23:55:58 2017 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Tue Jun 06 13:13:25 2017 +0200
     1.3 @@ -22,7 +22,6 @@
     1.4    val thms_of_name : Proof.context -> string -> thm list
     1.5    val one_day : Time.time
     1.6    val one_year : Time.time
     1.7 -  val with_vanilla_print_mode : ('a -> 'b) -> 'a -> 'b
     1.8    val hackish_string_of_term : Proof.context -> term -> string
     1.9    val spying : bool -> (unit -> Proof.state * int * string * string) -> unit
    1.10  end;
    1.11 @@ -138,12 +137,9 @@
    1.12  val one_day = seconds (24.0 * 60.0 * 60.0)
    1.13  val one_year = seconds (365.0 * 24.0 * 60.0 * 60.0)
    1.14  
    1.15 -fun with_vanilla_print_mode f x =
    1.16 -  Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
    1.17 -
    1.18  fun hackish_string_of_term ctxt =
    1.19    (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
    1.20 -  #> *) with_vanilla_print_mode (Syntax.string_of_term ctxt)
    1.21 +  #> *) Print_Mode.setmp [] (Syntax.string_of_term ctxt)
    1.22    #> YXML.content_of
    1.23    #> simplify_spaces
    1.24