src/ZF/Tools/induct_tacs.ML
changeset 6851 526c0b90bcef
parent 6556 daa00919502b
child 6970 ac37a8fcaad1
     1.1 --- a/src/ZF/Tools/induct_tacs.ML	Mon Jun 28 21:47:55 1999 +0200
     1.2 +++ b/src/ZF/Tools/induct_tacs.ML	Mon Jun 28 21:48:36 1999 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  
     1.5    fun print sg tab =
     1.6      Pretty.writeln (Pretty.strs ("datatypes:" ::
     1.7 -      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
     1.8 +      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
     1.9    end;
    1.10  
    1.11  structure DatatypesData = TheoryDataFun(DatatypesArgs);