# HG changeset patch
# User wenzelm
# Date 973879614 -3600
# Node ID 6c3901071d67d9096a3dda3f14b88dd3ad3dbcd9
# Parent  7528f9e30ca48ed02752845cc84b422596884375
Sign.certify_tycon, Sign.certify_const;

diff -r 7528f9e30ca4 -r 6c3901071d67 src/HOL/Tools/induct_attrib.ML
--- 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