diff -r 0d728eadad86 -r ece9fe9bf440 src/Pure/Syntax/ast.ML
--- 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];