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