src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 37146 f652333bbf8e
parent 37145 01aa36932739
child 37172 365f2296ae5b
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -911,7 +911,7 @@
     1.4  fun string_for_proof ctxt i n =
     1.5    let
     1.6      fun fix_print_mode f =
     1.7 -      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
     1.8 +      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
     1.9                        (print_mode_value ())) f
    1.10      fun do_indent ind = replicate_string (ind * indent_size) " "
    1.11      fun do_free (s, T) =