src/HOL/Tools/induct_attrib.ML
changeset 10438 6c3901071d67
parent 10271 45b996639c45
child 10526 ced4f4ec917e
--- a/src/HOL/Tools/induct_attrib.ML	Fri Nov 10 19:06:30 2000 +0100
+++ b/src/HOL/Tools/induct_attrib.ML	Fri Nov 10 19:06:54 2000 +0100
@@ -160,8 +160,8 @@
 
 fun attrib sign_of add_type add_set = Scan.depend (fn x =>
   let val sg = sign_of x in
-    spec typeN >> (add_type o Sign.intern_tycon sg) ||
-    spec setN  >> (add_set o Sign.intern_const sg)
+    spec typeN >> (add_type o Sign.certify_tycon sg o Sign.intern_tycon sg) ||
+    spec setN  >> (add_set o Sign.certify_const sg o Sign.intern_const sg)
   end >> pair x);
 
 in