src/Pure/sign.ML
changeset 20548 8ef25fe585a8
parent 20330 6192478fdba5
child 20664 ffbc5a57191a
     1.1 --- a/src/Pure/sign.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/Pure/sign.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -461,7 +461,7 @@
     1.4    let
     1.5      val _ = Context.check_thy thy;
     1.6      val _ = check_vars tm;
     1.7 -    val tm' = Term.map_term_types (certify_typ thy) tm;
     1.8 +    val tm' = Term.map_types (certify_typ thy) tm;
     1.9      val T = type_check pp tm';
    1.10      val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
    1.11      val tm'' = Consts.certify pp (tsig_of thy) consts tm';