diff -r e5419ecf92b7 -r c10fb22a5e0c src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Tue Jun 01 11:01:16 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Tue Jun 01 11:04:49 2010 +0200
@@ -243,7 +243,7 @@
       | NONE => I
   in
     thy
-    |> AxClass.add_classrel classrel
+    |> AxClass.add_classrel true classrel
     |> ClassData.map (Graph.add_edge (sub, sup))
     |> activate_defs sub (these_defs thy diff_sort)
     |> add_dependency
@@ -366,7 +366,7 @@
 fun gen_classrel mk_prop classrel thy =
   let
     fun after_qed results =
-      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
+      ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results);
   in
     thy
     |> ProofContext.init_global
@@ -531,7 +531,7 @@
     val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
     val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
     fun after_qed' results =
-      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
+      Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results)
       #> after_qed;
   in
     lthy
@@ -591,7 +591,7 @@
     val sorts = map snd vs;
     val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
     fun after_qed results = ProofContext.theory
-      ((fold o fold) AxClass.add_arity results);
+      ((fold o fold) (AxClass.add_arity true) results);
   in
     thy
     |> ProofContext.init_global