src/HOL/Tools/recdef_package.ML
changeset 6851 526c0b90bcef
parent 6729 b6e167580a32
child 7262 a05dc63ca29b
--- 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);