--- a/src/Pure/Isar/proof_context.ML Wed Apr 04 00:11:18 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Apr 04 00:11:20 2007 +0200
@@ -290,7 +290,7 @@
val thy = theory_of ctxt;
val syntax = syntax_of ctxt;
val consts = consts_of ctxt;
- val do_abbrevs = abbrevs andalso not (Output.has_mode "no_abbrevs");
+ val do_abbrevs = abbrevs andalso not (print_mode_active "no_abbrevs");
val t' = t
|> do_abbrevs ? rewrite_term true thy (Consts.abbrevs_of consts (! print_mode @ [""]))
|> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [Syntax.internalM])
--- a/src/Pure/ProofGeneral/preferences.ML Wed Apr 04 00:11:18 2007 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Wed Apr 04 00:11:20 2007 +0200
@@ -66,7 +66,7 @@
val thm_deps_pref =
let
- fun get () = PgipTypes.bool_to_pgstring (Output.has_mode thm_depsN)
+ fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
fun set s = if PgipTypes.read_pgipbool s then
change print_mode (insert (op =) thm_depsN)
else