src/Pure/Isar/isar_cmd.ML
changeset 37146 f652333bbf8e
parent 36950 75b8f26f2f07
child 37198 3af985b10550
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4  
     1.5  fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
     1.6    (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
     1.7 -    PrintMode.with_modes modes (Toplevel.print_state true) state));
     1.8 +    Print_Mode.with_modes modes (Toplevel.print_state true) state));
     1.9  
    1.10  val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
    1.11  val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
    1.12 @@ -488,7 +488,7 @@
    1.13    in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
    1.14  
    1.15  fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
    1.16 -  PrintMode.with_modes modes (fn () =>
    1.17 +  Print_Mode.with_modes modes (fn () =>
    1.18      writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
    1.19  
    1.20  in