diff -r 1e5b4c66317f -r 1f053d05f571 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Oct 20 16:25:54 1998 +0200
+++ b/src/Pure/pure_thy.ML	Tue Oct 20 16:26:20 1998 +0200
@@ -166,7 +166,7 @@
   in (next + 1, foldl add (table, consts)) end;
 
 fun make_const_idx thm_tab =
-  foldl (foldl add_const_idx) ((0, Symtab.empty), map snd (Symtab.dest thm_tab));
+  Symtab.foldl (fn (x, (_, ths)) => foldl add_const_idx (x, ths)) ((0, Symtab.empty), thm_tab);
 
 
 (* lookup index *)