src/ZF/Tools/induct_tacs.ML

--- a/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:47 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:48 2005 +0200
@@ -42,7 +42,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map #1 (Sign.extern_table sg Sign.typeK tab)));
+      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
   end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);