# HG changeset patch
# User wenzelm
# Date 1527883303 -7200
# Node ID bcdc4c21ab1dd60e7e36ef39e720e2f4867e6696
# Parent  7fafc8a01915b7c9074510e6b4d482e106489fb1
varify frees, notably dangling_params (see also e0cd57aeb60c);

diff -r 7fafc8a01915 -r bcdc4c21ab1d src/Pure/Isar/class.ML
--- 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;