src/Pure/consts.ML
changeset 37146 f652333bbf8e
parent 35680 897740382442
child 40722 441260986b63
--- a/src/Pure/consts.ML	Thu May 27 17:41:27 2010 +0200
+++ b/src/Pure/consts.ML	Thu May 27 18:10:37 2010 +0200
@@ -270,7 +270,7 @@
   let
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
-    val force_expand = mode = PrintMode.internal;
+    val force_expand = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));