equal
deleted
inserted
replaced
164 fun add (tab, c) = |
164 fun add (tab, c) = |
165 Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab); |
165 Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab); |
166 in (next + 1, foldl add (table, consts)) end; |
166 in (next + 1, foldl add (table, consts)) end; |
167 |
167 |
168 fun make_const_idx thm_tab = |
168 fun make_const_idx thm_tab = |
169 foldl (foldl add_const_idx) ((0, Symtab.empty), map snd (Symtab.dest thm_tab)); |
169 Symtab.foldl (fn (x, (_, ths)) => foldl add_const_idx (x, ths)) ((0, Symtab.empty), thm_tab); |
170 |
170 |
171 |
171 |
172 (* lookup index *) |
172 (* lookup index *) |
173 |
173 |
174 (*search locally*) |
174 (*search locally*) |