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));