tuned -- more explicit expression;

--- 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