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