# HG changeset patch
# User wenzelm
# Date 1704840110 -3600
# Node ID ca2fe94e8048facac8b609addb2d42c3c8d1ef2e
# Parent  3d867a43041308b9b2039e14aba1d834c65adc4b
tuned whitespace;

diff -r 3d867a430413 -r ca2fe94e8048 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Jan 09 23:40:53 2024 +0100
+++ b/src/Pure/consts.ML	Tue Jan 09 23:41:50 2024 +0100
@@ -304,9 +304,7 @@
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
 
-    val rhs = raw_rhs
-      |> cert_term
-      |> Term.close_schematic_term;
+    val rhs = raw_rhs |> cert_term |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;
     val T = Term.fastype_of rhs;
     val lhs = Const (Name_Space.full_name (Name_Space.naming_of context) b, T);