src/Pure/Isar/proof_context.ML

   val name = "Isar/proof_data";
   type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
 
   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;
   fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
 end;