src/ZF/Tools/induct_tacs.ML
changeset 16364 dc9f7066d80a
parent 16122 864fda4a4056
child 16458 4c6fd0c01d28
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:47 2005 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sat Jun 11 22:15:48 2005 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5    fun print sg tab =
     1.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     1.7 -      map #1 (Sign.extern_table sg Sign.typeK tab)));
     1.8 +      map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
     1.9    end;
    1.10  
    1.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);