src/Pure/Isar/class.ML

 struct
 
 (** auxiliary **)
 
 fun prove_interpretation tac prfx_atts expr inst =
-  Locale.interpretation_i I prfx_atts expr inst
+  Locale.interpretation I prfx_atts expr inst
   ##> Proof.global_terminal_proof
       (Method.Basic (fn ctxt => Method.SIMPLE_METHOD (tac ctxt), Position.none), NONE)
   ##> ProofContext.theory_of;
 
 fun prove_interpretation_in tac after_qed (name, expr) =

       (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   #> ProofContext.theory_of;
 
 val class_prefix = Logic.const_of_class o Sign.base_name;
 
+fun class_name_morphism class =
+  Name.map_prefix (K (Name.add_prefix false (class_prefix class)));
+
 fun activate_class_morphism thy class inst morphism =
-  Locale.get_interpret_morph thy class (false, class_prefix class) "" morphism class inst;
+  Locale.get_interpret_morph thy (class_name_morphism class) (class, "") morphism class inst;
 
 fun prove_class_interpretation class inst consts hyp_facts def_facts thy =
   let
     val constraints = map (fn (class, c) => map_atyps (K (TFree (Name.aT,
       [class]))) (Sign.the_const_type thy c)) consts;

       ORELSE' (fn n => SELECT_GOAL (Locale.intro_locales_tac false ctxt []) n));
     val prfx = class_prefix class;
   in
     thy
     |> fold2 add_constraint (map snd consts) no_constraints
-    |> prove_interpretation tac (false, prfx) (Locale.Locale class)
+    |> prove_interpretation tac (class_name_morphism class) (Locale.Locale class)
           (map SOME inst, map (pair (Attrib.no_binding) o Thm.prop_of) def_facts)
     ||> fold2 add_constraint (map snd consts) constraints
   end;
 
 

     val (((sups, supparams), (supsort, base_sort, mergeexpr)), (elems, global_syntax)) =
       prep_spec thy raw_supclasses raw_elems;
     val supconsts = map (apsnd fst o snd) (these_params thy sups);
   in
     thy
-    |> Locale.add_locale_i "" bname mergeexpr elems
+    |> Locale.add_locale "" bname mergeexpr elems
     |> snd
     |> ProofContext.theory_of
     |> adjungate_axclass bname class base_sort sups supsort supparams global_syntax
     |-> (fn (inst, param_map, params, assm_axiom) =>
         `(fn thy => calculate_axiom thy sups base_sort assm_axiom param_map class)