| changeset 12123 | 739eba13e2cd |
| parent 12100 | bb10ac677955 |
| child 12130 | 30d9143aff7e |
--- a/src/Pure/Isar/proof_context.ML Fri Nov 09 00:18:23 2001 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Nov 09 00:19:20 2001 +0100 @@ -212,6 +212,7 @@ val empty = Symtab.empty; val copy = I; + val finish = I; val prep_ext = I; fun merge tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs handle Symtab.DUPS kinds => err_inconsistent kinds;