src/Pure/Isar/outer_syntax.ML

 
 structure Data = Theory_Data
 (
   type T = command Symtab.table;
   val empty = Symtab.empty;
-  val extend = I;
   fun merge data : T =
     data |> Symtab.join (fn name => fn (cmd1, cmd2) =>
       if eq_command (cmd1, cmd2) then raise Symtab.SAME
       else err_dup_command name [command_pos cmd1, command_pos cmd2]);
 );