varify frees, notably dangling_params (see also e0cd57aeb60c);

--- a/src/Pure/Isar/class.ML	Fri Jun 01 22:00:50 2018 +0200
+++ b/src/Pure/Isar/class.ML	Fri Jun 01 22:01:43 2018 +0200
@@ -377,7 +377,7 @@
 fun global_def (b, eq) thy =
   let
     val ((_, def_thm), thy') = thy |> Thm.add_def_global false false (b, eq);
-    val def_thm' = def_thm |> Thm.varifyT_global;
+    val def_thm' = def_thm |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 |> Thm.varifyT_global;
     val (_, thy'') = thy' |> Global_Theory.store_thm (b, def_thm');
   in (def_thm', thy'') end;