diff -r 19962431aea8 -r 006cb47a2700 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue May 09 16:59:20 2023 +0200
+++ b/src/Pure/Syntax/parser.ML	Tue May 09 19:35:46 2023 +0200
@@ -7,7 +7,6 @@
 
 signature PARSER =
 sig
-  val timing: bool Unsynchronized.ref
   type gram
   val empty_gram: gram
   val extend_gram: Syntax_Ext.xprod list -> gram -> gram
@@ -416,8 +415,6 @@
 
 (** operations on grammars **)
 
-val timing = Unsynchronized.ref true;
-
 val empty_gram =
   Gram
    {nt_count = 0,
@@ -429,8 +426,8 @@
 
 
 (*Add productions to a grammar*)
-fun extend_gram0 [] gram = gram
-  | extend_gram0 xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
+fun extend_gram [] gram = gram
+  | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =
       let
         (*Get tag for existing nonterminal or create a new one*)
         fun get_tag nt_count tags nt =
@@ -493,12 +490,6 @@
           prods = Array.vector prods'}
       end;
 
-fun extend_gram xprods gram =
-  if ! timing then
-    Timing.cond_timeit true ("Parser.extend_gram" ^ Position.here (Position.thread_data ()))
-      (fn () => extend_gram0 xprods gram)
-  else extend_gram0 xprods gram;
-
 fun make_gram xprods = extend_gram xprods empty_gram;