src/Pure/Syntax/syntax.ML
changeset 81152 ece9fe9bf440
parent 81116 0fb1e2dd4122
child 81163 2301ec62fdca
--- 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);