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