diff -r 65258d2c3214 -r e5980f0ad025 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Mar 20 02:23:41 2010 +0100
+++ b/src/Pure/Isar/class.ML	Sat Mar 20 17:33:11 2010 +0100
@@ -257,7 +257,7 @@
         | t => t);
     val raw_pred = Locale.intros_of thy class
       |> fst
-      |> Option.map (Logic.unvarify o Logic.strip_imp_concl o Thm.prop_of);
+      |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
     fun get_axiom thy = case (#axioms o AxClass.get_info thy) class
      of [] => NONE
       | [thm] => SOME thm;