src/Pure/Isar/class_declaration.ML

        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
        Context.theory_map (Locale.add_registration (class, base_morph)
          (Option.map (rpair true) eq_morph) export_morph)
     #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> Named_Target.init (SOME class)
+    |> Named_Target.init class
     |> pair class
   end;
 
 in
 

     val some_prop = try the_single props;
     val some_dep_morph = try the_single (map snd deps);
     fun after_qed some_wit =
       ProofContext.theory (Class.register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> Named_Target.init (SOME sub);
+      #> ProofContext.theory_of #> Named_Target.init sub;
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
   Element.witness_proof (after_qed o try the_single o the_single)
     [the_list some_prop];