# HG changeset patch
# User wenzelm
# Date 1527883250 -7200
# Node ID 7fafc8a01915b7c9074510e6b4d482e106489fb1
# Parent  30d6ffd0ca071527903d3d413bcf7a8dfac62583
tuned -- more explicit expression;

diff -r 30d6ffd0ca07 -r 7fafc8a01915 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Jun 01 15:57:28 2018 +0200
+++ b/src/Pure/Isar/class.ML	Fri Jun 01 22:00:50 2018 +0200
@@ -375,12 +375,11 @@
   in (type_params, dangling_term_params) end;
 
 fun global_def (b, eq) thy =
-  thy
-  |> Thm.add_def_global false false (b, eq)
-  |>> (Thm.varifyT_global o snd)
-  |-> (fn def_thm => Global_Theory.store_thm (b, def_thm)
-      #> snd
-      #> pair def_thm);
+  let
+    val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq);
+    val def_thm' = def_thm |> Thm.varifyT_global;
+    val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm');
+  in (def_thm', thy'') end;
 
 fun canonical_const class phi dangling_params ((b, mx), rhs) thy =
   let