# HG changeset patch
# User wenzelm
# Date 1633360937 -7200
# Node ID f5c5006d142e4528fc63352254268cb36f36a3d3
# Parent  7fada501211b8a23ac6b5cc6f6279c7f50322f33
tuned;

diff -r 7fada501211b -r f5c5006d142e src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 17:09:12 2021 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Mon Oct 04 17:22:17 2021 +0200
@@ -129,8 +129,7 @@
 
 fun abs_tr [Free x, t] = absfree_proper x t
   | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
-  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
-      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
+  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
@@ -140,9 +139,7 @@
   let
     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
-      | binder_tr [x, t] =
-          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
-          in Syntax.const name $ abs end
+      | binder_tr [x, t] = Syntax.const name $ (abs_tr [x, t] handle TERM _ => err [x, t])
       | binder_tr ts = err ts;
   in (syn, fn _ => binder_tr) end;