Symtab.foldl;
authorwenzelm
Tue, 20 Oct 1998 16:26:20 +0200
changeset 5686 1f053d05f571
parent 5685 1e5b4c66317f
child 5687 33ae54c0c821
Symtab.foldl;
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 *)