# HG changeset patch
# User wenzelm
# Date 1727558610 -7200
# Node ID addebc07f06e7a676a9ed43c751e227241553985
# Parent  fc0f2053c4d2aa6f9105f7386db3c17b72880433
tuned whitespace;

diff -r fc0f2053c4d2 -r addebc07f06e src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 21:16:01 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 23:23:30 2024 +0200
@@ -523,23 +523,19 @@
   Tip of Lexicon.token;
 
 local
-
-fun cons_nr (Node _) = 0
-  | cons_nr (Tip _) = 1;
-
+  fun cons_nr (Node _) = 0
+    | cons_nr (Tip _) = 1;
 in
-
-fun tree_ord trees =
-  if pointer_eq trees then EQUAL
-  else
-    (case trees of
-      (Node (s, ts), Node (s', ts')) =>
-        (case fast_string_ord (s, s') of
-          EQUAL => list_ord tree_ord (ts, ts')
-        | ord => ord)
-    | (Tip t, Tip t') => Lexicon.token_ord (t, t')
-    | _ => int_ord (apply2 cons_nr trees));
-
+  fun tree_ord trees =
+    if pointer_eq trees then EQUAL
+    else
+      (case trees of
+        (Node (s, ts), Node (s', ts')) =>
+          (case fast_string_ord (s, s') of
+            EQUAL => list_ord tree_ord (ts, ts')
+          | ord => ord)
+      | (Tip t, Tip t') => Lexicon.token_ord (t, t')
+      | _ => int_ord (apply2 cons_nr trees));
 end;
 
 fun pretty_tree (Node (c, ts)) =