src/Pure/Tools/class_package.ML

     |> Locale.interpretation I (prfx, atts) expr (map (Option.map ad_hoc_term) insts)
     |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
     |> ProofContext.theory_of
   end;
 
-(*
 fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   let
     val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
     val supclasses = map (prep_class thy) raw_supclasses;
     val supsort =

       Locale.parameters_of thy name_locale
       |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, [])))
       |> (map o apsnd) (TheoryTarget.fork_mixfix false true #> fst)
       |> chop (length supconsts)
       |> snd;
-    val LOC_AXIOMS = ref [] : string list ref;
     fun extract_assumes name_locale params thy cs =
       let
         val consts = supconsts @ (map (fst o fst) params ~~ cs);
         (*FIXME is this type handling correct?*)
         fun subst (Free (c, ty)) =
-          Const ((fst o the o AList.lookup (op =) consts) c, ty);
+              Const ((fst o the o AList.lookup (op =) consts) c, ty)
+          | subst t = t;
         fun prep_asm ((name, atts), ts) =
           (*FIXME*)
           ((NameSpace.base name, map (Attrib.attribute thy) atts), (map o map_aterms) subst ts);
       in
         Locale.local_asms_of thy name_locale
         |> map prep_asm
-        |> tap (fn assms => LOC_AXIOMS := map (fst o fst) assms)
       end;
+    fun extract_axiom_names thy name_locale =
+      name_locale
+      |> Locale.local_asms_of thy
+      |> map (NameSpace.base o fst o fst) (*FIXME*)
     fun mk_const thy class (c, ty) =
       Const (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty);
   in
     thy
     |> add_locale bname supexpr elems

       tap (fn thy => check_locale thy name_locale)
       #> `(fn thy => extract_params thy name_locale)
       #-> (fn params =>
         axclass_params (bname, supsort) params (extract_assumes name_locale params)
       #-> (fn (name_axclass, ((_, ax_axioms), consts)) =>
-        add_class_data ((name_axclass, supclasses), (name_locale, map (fst o fst) params ~~ map fst consts,
-            ! LOC_AXIOMS))
+        `(fn thy => extract_axiom_names thy name_locale)
+      #-> (fn axiom_names =>
+        add_class_data ((name_axclass, supclasses),
+          (name_locale, map (fst o fst) params ~~ map fst consts, axiom_names))
       #> prove_interpretation (Logic.const_of_class bname, [])
             (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd supconsts @ consts))
             ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
       #> pair name_axclass
-      ))))
-  end;
-*)
-
-fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
+      )))))
+  end;
+
+(*fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   let
     val elems = fold_rev (fn Locale.Elem e => cons e | _ => I) raw_elems [];
     val supclasses = map (prep_class thy) raw_supclasses;
     val supsort =
       supclasses

           map (fst o fst) loc_axioms))
     #> prove_interpretation (Logic.const_of_class bname, [])
           (Locale.Locale name_locale) (map (SOME o mk_const thy name_axclass) (map snd (mapp_sup @ mapp_this)))
           ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
     ))))) #> pair name_locale)
-  end;
+  end;*)
 
 in
 
 val class_e = gen_class (Locale.add_locale false) read_class;
 val class = gen_class (Locale.add_locale_i false) certify_class;