renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
authorwenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146f652333bbf8e
parent 37145 01aa36932739
child 37147 0c0ef115c7aa
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
NEWS
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Modelcheck/EindhovenSyn.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOLCF/IOA/meta_theory/automaton.ML
src/Pure/General/print_mode.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/theory_target.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ROOT.ML
src/Pure/Syntax/syntax.ML
src/Pure/Thy/html.ML
src/Pure/Thy/thy_output.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Tools/Code/code_printer.ML
src/Tools/WWW_Find/html_unicode.ML
src/Tools/nbe.ML
src/Tools/value.ML
     1.1 --- a/NEWS	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/NEWS	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -503,6 +503,7 @@
     1.4    OuterSyntax   ~>  Outer_Syntax
     1.5    SpecParse     ~>  Parse_Spec
     1.6    TypeInfer     ~>  Type_Infer
     1.7 +  PrintMode     ~>  Print_Mode
     1.8  
     1.9  Note that "open Legacy" simplifies porting of sources, but forgetting
    1.10  to remove it again will complicate porting again in the future.
     2.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 17:41:27 2010 +0200
     2.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Thu May 27 18:10:37 2010 +0200
     2.3 @@ -148,7 +148,7 @@
     2.4  ML {*
     2.5    fun check_syntax ctxt thm expected =
     2.6      let
     2.7 -      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
     2.8 +      val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
     2.9      in
    2.10        if obtained <> expected
    2.11        then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
     3.1 --- a/src/HOL/Import/proof_kernel.ML	Thu May 27 17:41:27 2010 +0200
     3.2 +++ b/src/HOL/Import/proof_kernel.ML	Thu May 27 18:10:37 2010 +0200
     3.3 @@ -200,7 +200,7 @@
     3.4                             handle TERM _ => ct)
     3.5      in
     3.6          quote (
     3.7 -        PrintMode.setmp [] (
     3.8 +        Print_Mode.setmp [] (
     3.9          setmp_CRITICAL show_brackets false (
    3.10          setmp_CRITICAL show_all_types true (
    3.11          setmp_CRITICAL Syntax.ambiguity_is_error false (
    3.12 @@ -239,14 +239,14 @@
    3.13                | SMART_STRING =>
    3.14                    error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
    3.15      in
    3.16 -      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    3.17 +      Print_Mode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    3.18      end
    3.19      handle ERROR mesg => simple_smart_string_of_cterm ct
    3.20  
    3.21  val smart_string_of_thm = smart_string_of_cterm o cprop_of
    3.22  
    3.23 -fun prth th = writeln (PrintMode.setmp [] Display.string_of_thm_without_context th);
    3.24 -fun prin t = writeln (PrintMode.setmp []
    3.25 +fun prth th = writeln (Print_Mode.setmp [] Display.string_of_thm_without_context th);
    3.26 +fun prin t = writeln (Print_Mode.setmp []
    3.27    (fn () => Syntax.string_of_term (ML_Context.the_local_context ()) t) ());
    3.28  fun pth (HOLThm(ren,thm)) =
    3.29      let
     4.1 --- a/src/HOL/Import/shuffler.ML	Thu May 27 17:41:27 2010 +0200
     4.2 +++ b/src/HOL/Import/shuffler.ML	Thu May 27 18:10:37 2010 +0200
     4.3 @@ -56,7 +56,7 @@
     4.4  (*Prints an exception, then fails*)
     4.5  fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise e)
     4.6  
     4.7 -val string_of_thm = PrintMode.setmp [] Display.string_of_thm_without_context;
     4.8 +val string_of_thm = Print_Mode.setmp [] Display.string_of_thm_without_context;
     4.9  
    4.10  fun mk_meta_eq th =
    4.11      (case concl_of th of
     5.1 --- a/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 17:41:27 2010 +0200
     5.2 +++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Thu May 27 18:10:37 2010 +0200
     5.3 @@ -32,7 +32,7 @@
     5.4  oracle mc_eindhoven_oracle =
     5.5  {*
     5.6  let
     5.7 -  val eindhoven_term = PrintMode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
     5.8 +  val eindhoven_term = Print_Mode.setmp ["Eindhoven"] o Syntax.string_of_term_global;
     5.9  
    5.10    fun call_mc s =
    5.11      let
     6.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 17:41:27 2010 +0200
     6.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu May 27 18:10:37 2010 +0200
     6.3 @@ -487,7 +487,7 @@
     6.4          make_string sign (trm::list) =
     6.5             Syntax.string_of_term_global sign trm ^ "\n" ^ make_string sign list
     6.6  in
     6.7 -  PrintMode.setmp ["Mucke"] (make_string sign) terms
     6.8 +  Print_Mode.setmp ["Mucke"] (make_string sign) terms
     6.9  end;
    6.10  
    6.11  fun callmc s =
     7.1 --- a/src/HOL/Statespace/state_space.ML	Thu May 27 17:41:27 2010 +0200
     7.2 +++ b/src/HOL/Statespace/state_space.ML	Thu May 27 18:10:37 2010 +0200
     7.3 @@ -439,7 +439,7 @@
     7.4  
     7.5     fun string_of_typ T =
     7.6        setmp_CRITICAL show_sorts true
     7.7 -       (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
     7.8 +       (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
     7.9     val fixestate = (case state_type of
    7.10           NONE => []
    7.11         | SOME s =>
     8.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 17:41:27 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu May 27 18:10:37 2010 +0200
     8.3 @@ -483,7 +483,7 @@
     8.4          val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
     8.5          val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
     8.6          val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
     8.7 -                      PrintMode.setmp [] multiline_string_for_scope scope
     8.8 +                      Print_Mode.setmp [] multiline_string_for_scope scope
     8.9          val kodkod_sat_solver =
    8.10            Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd
    8.11          val bit_width = if bits = 0 then 16 else bits + 1
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 17:41:27 2010 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 27 18:10:37 2010 +0200
     9.3 @@ -3306,7 +3306,7 @@
     9.4               Pretty.str "total:", Pretty.brk 1, Pretty.str (string_of_int total), Pretty.fbrk]
     9.5               @ maps pretty_entry xs
     9.6            end
     9.7 -    val p = PrintMode.with_modes print_modes (fn () =>
     9.8 +    val p = Print_Mode.with_modes print_modes (fn () =>
     9.9        Pretty.block ([Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
    9.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]
    9.11          @ pretty_stat)) ();
    10.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 17:41:27 2010 +0200
    10.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu May 27 18:10:37 2010 +0200
    10.3 @@ -911,7 +911,7 @@
    10.4  fun string_for_proof ctxt i n =
    10.5    let
    10.6      fun fix_print_mode f =
    10.7 -      PrintMode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    10.8 +      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    10.9                        (print_mode_value ())) f
   10.10      fun do_indent ind = replicate_string (ind * indent_size) " "
   10.11      fun do_free (s, T) =
    11.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 17:41:27 2010 +0200
    11.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu May 27 18:10:37 2010 +0200
    11.3 @@ -18,8 +18,8 @@
    11.4  structure Automaton: AUTOMATON =
    11.5  struct
    11.6  
    11.7 -val string_of_typ = PrintMode.setmp [] o Syntax.string_of_typ_global;
    11.8 -val string_of_term = PrintMode.setmp [] o Syntax.string_of_term_global;
    11.9 +val string_of_typ = Print_Mode.setmp [] o Syntax.string_of_typ_global;
   11.10 +val string_of_term = Print_Mode.setmp [] o Syntax.string_of_term_global;
   11.11  
   11.12  exception malformed;
   11.13  
    12.1 --- a/src/Pure/General/print_mode.ML	Thu May 27 17:41:27 2010 +0200
    12.2 +++ b/src/Pure/General/print_mode.ML	Thu May 27 18:10:37 2010 +0200
    12.3 @@ -22,7 +22,7 @@
    12.4    val closure: ('a -> 'b) -> 'a -> 'b
    12.5  end;
    12.6  
    12.7 -structure PrintMode: PRINT_MODE =
    12.8 +structure Print_Mode: PRINT_MODE =
    12.9  struct
   12.10  
   12.11  val input = "input";
   12.12 @@ -49,5 +49,5 @@
   12.13  
   12.14  end;
   12.15  
   12.16 -structure BasicPrintMode: BASIC_PRINT_MODE = PrintMode;
   12.17 -open BasicPrintMode;
   12.18 +structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
   12.19 +open Basic_Print_Mode;
    13.1 --- a/src/Pure/Isar/class_target.ML	Thu May 27 17:41:27 2010 +0200
    13.2 +++ b/src/Pure/Isar/class_target.ML	Thu May 27 18:10:37 2010 +0200
    13.3 @@ -355,7 +355,7 @@
    13.4      |> snd
    13.5      |> Sign.add_const_constraint (c', SOME ty')
    13.6      |> Sign.notation true prmode [(Const (c', ty'), mx)]
    13.7 -    |> not (#1 prmode = PrintMode.input) ? register_operation class (c', (rhs', NONE))
    13.8 +    |> not (#1 prmode = Print_Mode.input) ? register_operation class (c', (rhs', NONE))
    13.9    end;
   13.10  
   13.11  
    14.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 17:41:27 2010 +0200
    14.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 18:10:37 2010 +0200
    14.3 @@ -281,7 +281,7 @@
    14.4  
    14.5  fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state =>
    14.6    (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false;
    14.7 -    PrintMode.with_modes modes (Toplevel.print_state true) state));
    14.8 +    Print_Mode.with_modes modes (Toplevel.print_state true) state));
    14.9  
   14.10  val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true);
   14.11  val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false);
   14.12 @@ -488,7 +488,7 @@
   14.13    in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
   14.14  
   14.15  fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
   14.16 -  PrintMode.with_modes modes (fn () =>
   14.17 +  Print_Mode.with_modes modes (fn () =>
   14.18      writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
   14.19  
   14.20  in
    15.1 --- a/src/Pure/Isar/theory_target.ML	Thu May 27 17:41:27 2010 +0200
    15.2 +++ b/src/Pure/Isar/theory_target.ML	Thu May 27 18:10:37 2010 +0200
    15.3 @@ -200,8 +200,8 @@
    15.4    in
    15.5      not (is_class andalso (same_shape orelse class_global)) ?
    15.6        (Context.mapping_result
    15.7 -        (Sign.add_abbrev PrintMode.internal arg)
    15.8 -        (ProofContext.add_abbrev PrintMode.internal arg)
    15.9 +        (Sign.add_abbrev Print_Mode.internal arg)
   15.10 +        (ProofContext.add_abbrev Print_Mode.internal arg)
   15.11        #-> (fn (lhs' as Const (d, _), _) =>
   15.12            same_shape ?
   15.13              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
   15.14 @@ -225,7 +225,7 @@
   15.15    in
   15.16      lthy |>
   15.17       (if is_locale then
   15.18 -        Local_Theory.theory_result (Sign.add_abbrev PrintMode.internal (b, global_rhs))
   15.19 +        Local_Theory.theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs))
   15.20          #-> (fn (lhs, _) =>
   15.21            let val lhs' = Term.list_comb (Logic.unvarify_global lhs, xs) in
   15.22              syntax_declaration ta false (locale_const ta prmode ((b, mx2), lhs')) #>
   15.23 @@ -235,7 +235,7 @@
   15.24          Local_Theory.theory
   15.25            (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) =>
   15.26             Sign.notation true prmode [(lhs, mx3)])))
   15.27 -    |> ProofContext.add_abbrev PrintMode.internal (b, t) |> snd
   15.28 +    |> ProofContext.add_abbrev Print_Mode.internal (b, t) |> snd
   15.29      |> Local_Defs.fixed_abbrev ((b, NoSyn), t)
   15.30    end;
   15.31  
    16.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 17:41:27 2010 +0200
    16.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Thu May 27 18:10:37 2010 +0200
    16.3 @@ -93,7 +93,7 @@
    16.4    let
    16.5      val kind = ThySyntax.span_kind span;
    16.6      val toks = ThySyntax.span_content span;
    16.7 -    val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
    16.8 +    val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
    16.9    in
   16.10      (case kind of
   16.11        ThySyntax.Command name => parse_command name text
    17.1 --- a/src/Pure/ROOT.ML	Thu May 27 17:41:27 2010 +0200
    17.2 +++ b/src/Pure/ROOT.ML	Thu May 27 18:10:37 2010 +0200
    17.3 @@ -310,6 +310,7 @@
    17.4  structure OuterSyntax = Outer_Syntax;
    17.5  structure SpecParse = Parse_Spec;
    17.6  structure TypeInfer = Type_Infer;
    17.7 +structure PrintMode = Print_Mode;
    17.8  
    17.9  end;
   17.10  
    18.1 --- a/src/Pure/Syntax/syntax.ML	Thu May 27 17:41:27 2010 +0200
    18.2 +++ b/src/Pure/Syntax/syntax.ML	Thu May 27 18:10:37 2010 +0200
    18.3 @@ -259,7 +259,7 @@
    18.4  
    18.5  type mode = string * bool;
    18.6  val mode_default = ("", true);
    18.7 -val mode_input = (PrintMode.input, true);
    18.8 +val mode_input = (Print_Mode.input, true);
    18.9  
   18.10  
   18.11  (* empty_syntax *)
    19.1 --- a/src/Pure/Thy/html.ML	Thu May 27 17:41:27 2010 +0200
    19.2 +++ b/src/Pure/Thy/html.ML	Thu May 27 18:10:37 2010 +0200
    19.3 @@ -42,7 +42,7 @@
    19.4  (* mode *)
    19.5  
    19.6  val htmlN = "HTML";
    19.7 -fun html_mode f x = PrintMode.with_modes [htmlN] f x;
    19.8 +fun html_mode f x = Print_Mode.with_modes [htmlN] f x;
    19.9  
   19.10  
   19.11  (* common markup *)
    20.1 --- a/src/Pure/Thy/thy_output.ML	Thu May 27 17:41:27 2010 +0200
    20.2 +++ b/src/Pure/Thy/thy_output.ML	Thu May 27 18:10:37 2010 +0200
    20.3 @@ -153,7 +153,7 @@
    20.4        | expand (Antiquote.Antiq (ss, (pos, _))) =
    20.5            let val (opts, src) = Token.read_antiq lex antiq (ss, pos) in
    20.6              options opts (fn () => command src state) ();  (*preview errors!*)
    20.7 -            PrintMode.with_modes (! modes @ Latex.modes)
    20.8 +            Print_Mode.with_modes (! modes @ Latex.modes)
    20.9                (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
   20.10            end
   20.11        | expand (Antiquote.Open _) = ""
   20.12 @@ -429,7 +429,7 @@
   20.13    ("display", setmp_CRITICAL display o boolean),
   20.14    ("break", setmp_CRITICAL break o boolean),
   20.15    ("quotes", setmp_CRITICAL quotes o boolean),
   20.16 -  ("mode", fn s => fn f => PrintMode.with_modes [s] f),
   20.17 +  ("mode", fn s => fn f => Print_Mode.with_modes [s] f),
   20.18    ("margin", setmp_CRITICAL Pretty.margin_default o integer),
   20.19    ("indent", setmp_CRITICAL indent o integer),
   20.20    ("source", setmp_CRITICAL source o boolean),
    21.1 --- a/src/Pure/codegen.ML	Thu May 27 17:41:27 2010 +0200
    21.2 +++ b/src/Pure/codegen.ML	Thu May 27 18:10:37 2010 +0200
    21.3 @@ -109,9 +109,9 @@
    21.4  
    21.5  val margin = Unsynchronized.ref 80;
    21.6  
    21.7 -fun string_of p = PrintMode.setmp [] (Pretty.string_of_margin (!margin)) p;
    21.8 +fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
    21.9  
   21.10 -val str = PrintMode.setmp [] Pretty.str;
   21.11 +val str = Print_Mode.setmp [] Pretty.str;
   21.12  
   21.13  (**** Mixfix syntax ****)
   21.14  
    22.1 --- a/src/Pure/consts.ML	Thu May 27 17:41:27 2010 +0200
    22.2 +++ b/src/Pure/consts.ML	Thu May 27 18:10:37 2010 +0200
    22.3 @@ -270,7 +270,7 @@
    22.4    let
    22.5      val cert_term = certify pp tsig false consts;
    22.6      val expand_term = certify pp tsig true consts;
    22.7 -    val force_expand = mode = PrintMode.internal;
    22.8 +    val force_expand = mode = Print_Mode.internal;
    22.9  
   22.10      val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
   22.11        error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
    23.1 --- a/src/Tools/Code/code_printer.ML	Thu May 27 17:41:27 2010 +0200
    23.2 +++ b/src/Tools/Code/code_printer.ML	Thu May 27 18:10:37 2010 +0200
    23.3 @@ -105,19 +105,19 @@
    23.4  infixr 5 @|;
    23.5  fun x @@ y = [x, y];
    23.6  fun xs @| y = xs @ [y];
    23.7 -val str = PrintMode.setmp [] Pretty.str;
    23.8 +val str = Print_Mode.setmp [] Pretty.str;
    23.9  val concat = Pretty.block o Pretty.breaks;
   23.10 -fun enclose l r = PrintMode.setmp [] (Pretty.enclose l r);
   23.11 +fun enclose l r = Print_Mode.setmp [] (Pretty.enclose l r);
   23.12  val brackets = enclose "(" ")" o Pretty.breaks;
   23.13 -fun enum sep l r = PrintMode.setmp [] (Pretty.enum sep l r);
   23.14 +fun enum sep l r = Print_Mode.setmp [] (Pretty.enum sep l r);
   23.15  fun enum_default default sep l r [] = str default
   23.16    | enum_default default sep l r xs = enum sep l r xs;
   23.17  fun semicolon ps = Pretty.block [concat ps, str ";"];
   23.18  fun doublesemicolon ps = Pretty.block [concat ps, str ";;"];
   23.19 -fun indent i = PrintMode.setmp [] (Pretty.indent i);
   23.20 +fun indent i = Print_Mode.setmp [] (Pretty.indent i);
   23.21  
   23.22 -fun string_of_pretty width p = PrintMode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
   23.23 -fun writeln_pretty width p = writeln (PrintMode.setmp [] (Pretty.string_of_margin width) p);
   23.24 +fun string_of_pretty width p = Print_Mode.setmp [] (Pretty.string_of_margin width) p ^ "\n";
   23.25 +fun writeln_pretty width p = writeln (Print_Mode.setmp [] (Pretty.string_of_margin width) p);
   23.26  
   23.27  
   23.28  (** names and variable name contexts **)
    24.1 --- a/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 17:41:27 2010 +0200
    24.2 +++ b/src/Tools/WWW_Find/html_unicode.ML	Thu May 27 18:10:37 2010 +0200
    24.3 @@ -19,7 +19,7 @@
    24.4  (* mode *)
    24.5  
    24.6  val htmlunicodeN = "HTMLUnicode";
    24.7 -fun print_mode f x = PrintMode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
    24.8 +fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
    24.9  
   24.10  (* symbol output *)
   24.11  
    25.1 --- a/src/Tools/nbe.ML	Thu May 27 17:41:27 2010 +0200
    25.2 +++ b/src/Tools/nbe.ML	Thu May 27 18:10:37 2010 +0200
    25.3 @@ -620,7 +620,7 @@
    25.4      val t' = norm thy t;
    25.5      val ty' = Term.type_of t';
    25.6      val ctxt' = Variable.auto_fixes t ctxt;
    25.7 -    val p = PrintMode.with_modes modes (fn () =>
    25.8 +    val p = Print_Mode.with_modes modes (fn () =>
    25.9        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   25.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   25.11    in Pretty.writeln p end;
    26.1 --- a/src/Tools/value.ML	Thu May 27 17:41:27 2010 +0200
    26.2 +++ b/src/Tools/value.ML	Thu May 27 18:10:37 2010 +0200
    26.3 @@ -47,7 +47,7 @@
    26.4        | SOME name => value_select name ctxt t;
    26.5      val ty' = Term.type_of t';
    26.6      val ctxt' = Variable.auto_fixes t' ctxt;
    26.7 -    val p = PrintMode.with_modes modes (fn () =>
    26.8 +    val p = Print_Mode.with_modes modes (fn () =>
    26.9        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   26.10          Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   26.11    in Pretty.writeln p end;