src/Pure/Isar/proof_context.ML
changeset 22587 5454b06320fb
parent 22358 4d8a9e3a29f8
child 22670 c803b2696ada
--- 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])