# HG changeset patch
# User wenzelm
# Date 930599316 -7200
# Node ID 526c0b90bcef427d8102324fdd5f10b518b77352
# Parent  da8a4660fb0cac152a8a506dd1efc0ca181ac10b
cond_extern_table;

diff -r da8a4660fb0c -r 526c0b90bcef src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Mon Jun 28 21:47:55 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Mon Jun 28 21:48:36 1999 +0200
@@ -92,7 +92,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
 end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);
diff -r da8a4660fb0c -r 526c0b90bcef src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Jun 28 21:47:55 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Jun 28 21:48:36 1999 +0200
@@ -167,7 +167,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("(co)inductives:" ::
-      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
+      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
 end;
 
 structure InductiveData = TheoryDataFun(InductiveArgs);
diff -r da8a4660fb0c -r 526c0b90bcef src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Mon Jun 28 21:47:55 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Mon Jun 28 21:48:36 1999 +0200
@@ -49,7 +49,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("recdefs:" ::
-      map (Sign.cond_extern sg Sign.constK o fst) (Symtab.dest tab)));
+      map #1 (Sign.cond_extern_table sg Sign.constK tab)));
 end;
 
 structure RecdefData = TheoryDataFun(RecdefArgs);
diff -r da8a4660fb0c -r 526c0b90bcef src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Jun 28 21:47:55 1999 +0200
+++ b/src/HOL/Tools/record_package.ML	Mon Jun 28 21:48:36 1999 +0200
@@ -359,9 +359,7 @@
       fun pretty_record (name, {args, parent, fields, simps = _}) = Pretty.block (Pretty.fbreaks
         (Pretty.block [prt_typ (Type (name, map TFree args)), Pretty.str " = "] ::
           pretty_parent parent @ map pretty_field fields));
-    in
-      seq (Pretty.writeln o pretty_record) (Symtab.dest recs)
-    end;
+    in seq (Pretty.writeln o pretty_record) (Sign.cond_extern_table sg Sign.typeK recs) end;
 end;
 
 structure RecordsData = TheoryDataFun(RecordsArgs);
diff -r da8a4660fb0c -r 526c0b90bcef src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Mon Jun 28 21:47:55 1999 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Mon Jun 28 21:48:36 1999 +0200
@@ -43,7 +43,7 @@
 
   fun print sg tab =
     Pretty.writeln (Pretty.strs ("datatypes:" ::
-      map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
+      map #1 (Sign.cond_extern_table sg Sign.typeK tab)));
   end;
 
 structure DatatypesData = TheoryDataFun(DatatypesArgs);