diff -r 0d728eadad86 -r ece9fe9bf440 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sat Oct 12 14:16:15 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sat Oct 12 14:22:19 2024 +0200
@@ -405,8 +405,8 @@
 
 fun dest_ruletab tab = Symtab.dest tab |> sort_by #1 |> maps #2;
 
-val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.head_of_rule r, r));
-val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
+val update_ruletab = fold_rev (fn r => Symtab.update_list (op =) (Ast.rule_index r, r));
+val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.rule_index r, r));
 fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);