src/Pure/Isar/constdefs.ML

--- a/src/Pure/Isar/constdefs.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -56,7 +56,7 @@
       |> Sign.add_consts_i [(b, T, mx)]
       |> PureThy.add_defs false [((name, def), atts)]
       |-> (fn [thm] =>  (* FIXME thm vs. atts !? *)
-        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
+        Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify_global head], [thm]) #>
         Code.add_default_eqn thm);
   in ((c, T), thy') end;