src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 37146 f652333bbf8e
parent 37135 636e6d8645d6
child 37391 476270a6c2dc
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -3306,7 +3306,7 @@
     1.4               Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
     1.5               @ maps pretty_entry xs
     1.6            end
     1.7 -    val p = PrintMode.with_modes print_modes (fn () =>
     1.8 +    val p = Print_Mode.with_modes print_modes (fn () =>
     1.9        Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    1.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
    1.11          @ pretty_stat)) ();