clarified signature;
tuned comments;

--- a/src/Pure/Syntax/ast.ML	Sat Oct 12 14:16:15 2024 +0200
+++ b/src/Pure/Syntax/ast.ML	Sat Oct 12 14:22:19 2024 +0200
@@ -18,7 +18,7 @@
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
   val strip_positions: ast -> ast
-  val head_of_rule: ast * ast -> string
+  val rule_index: ast * ast -> string
   val rule_error: ast * ast -> string option
   val fold_ast: string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
@@ -79,8 +79,7 @@
 structure Set = Set(Table.Key);
 
 
-
-(** print asts in a LISP-like style **)
+(* print asts in a LISP-like style *)
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) =
@@ -105,17 +104,11 @@
   | strip_positions ast = ast;
 
 
-(* head_of_ast and head_of_rule *)
-
-fun head_of_ast (Constant a) = a
-  | head_of_ast (Appl (Constant a :: _)) = a
-  | head_of_ast _ = "";
+(* translation rules *)
 
-fun head_of_rule (lhs, _) = head_of_ast lhs;
-
-
-
-(** check translation rules **)
+fun rule_index (Constant a, _: ast) = a
+  | rule_index (Appl (Constant a :: _), _) = a
+  | rule_index _ = "";
 
 fun rule_error (lhs, rhs) =
   let
@@ -132,10 +125,7 @@
   end;
 
 
-
-(** ast translation utilities **)
-
-(* fold asts *)
+(* ast translation utilities *)
 
 fun fold_ast _ [] = raise Match
   | fold_ast _ [y] = y
@@ -144,8 +134,6 @@
 fun fold_ast_p c = uncurry (fold_rev (fn x => fn xs => Appl [Constant c, x, xs]));
 
 
-(* unfold asts *)
-
 fun unfold_ast c (y as Appl [Constant c', x, xs]) =
       if c = c' then x :: unfold_ast c xs else [y]
   | unfold_ast _ y = [y];

--- 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);