src/Tools/value.ML
changeset 37146 f652333bbf8e
parent 36960 01594f816e3a
child 37744 3daaf23b9ab4
     1.1 --- a/src/Tools/value.ML	Thu May 27 17:41:27 2010 +0200
     1.2 +++ b/src/Tools/value.ML	Thu May 27 18:10:37 2010 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4        | SOME name => value_select name ctxt t;
     1.5      val ty' = Term.type_of t';
     1.6      val ctxt' = Variable.auto_fixes t' ctxt;
     1.7 -    val p = PrintMode.with_modes modes (fn () =>
     1.8 +    val p = Print_Mode.with_modes 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    in Pretty.writeln p end;