src/Pure/Isar/class_target.ML

      of SOME dep_morph => Locale.add_dependency sub
           (sup, dep_morph $> Element.satisfy_morphism (the_list some_wit)) export
       | 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
   end;
 

 local
 
 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
     |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
   end;

 fun gen_instantiation_instance do_proof after_qed lthy =
   let
     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
     |> do_proof after_qed' arities_proof
   end;

   let
     val (tycos, vs, sort) = read_multi_arity thy raw_arities;
     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
     |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   end;