--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 05 21:41:24 2010 +0200
@@ -947,11 +947,12 @@
fun string_for_proof ctxt0 full_types i n =
let
- val ctxt = Config.put show_free_types false ctxt0
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types true
fun fix_print_mode f x =
- setmp_CRITICAL show_types true
- (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f) x
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
maybe_quote s ^ " :: " ^