src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 61432 1502f2410d8b
parent 61330 20af2ad9261e
child 62826 eb94e570c1a4
equal deleted inserted replaced
61431:f6e314c1e9c4 61432:1502f2410d8b
   138 
   138 
   139 fun with_vanilla_print_mode f x =
   139 fun with_vanilla_print_mode f x =
   140   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
   140   Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) (print_mode_value ())) f x
   141 
   141 
   142 fun hackish_string_of_term ctxt =
   142 fun hackish_string_of_term ctxt =
   143   map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
   143   (* FIXME: map_aterms (fn Free (s, T) => Free (if Name.is_internal s then "_" else s, T) | t => t)
   144   #> with_vanilla_print_mode (Syntax.string_of_term ctxt)
   144   #> *) with_vanilla_print_mode (Syntax.string_of_term ctxt)
   145   #> YXML.content_of
   145   #> YXML.content_of
   146   #> simplify_spaces
   146   #> simplify_spaces
   147 
   147 
   148 val spying_version = "d"
   148 val spying_version = "d"
   149 
   149