1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 12:28:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jun 02 14:35:52 2010 +0200
     1.3 @@ -914,9 +914,11 @@
     1.4  
     1.5  fun string_for_proof ctxt i n =
     1.6    let
     1.7 -    fun fix_print_mode f =
     1.8 -      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
     1.9 -                      (print_mode_value ())) f
    1.10 +    fun fix_print_mode f x =
    1.11 +      setmp_CRITICAL show_no_free_types true
    1.12 +          (setmp_CRITICAL show_types true
    1.13 +               (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.14 +                                         (print_mode_value ())) f)) x
    1.15      fun do_indent ind = replicate_string (ind * indent_size) " "
    1.16      fun do_free (s, T) =
    1.17        maybe_quote s ^ " :: " ^