src/Pure/Tools/class_package.ML

 (* axclass instances *)
 
 local
 
 fun gen_instance mk_prop add_thm after_qed insts thy =
-  thy
-  |> ProofContext.init
-  |> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
-       ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts);
+  let
+    fun after_qed' results =
+      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
+  in
+    thy
+    |> ProofContext.init
+    |> Proof.theorem_i PureThy.internalK NONE after_qed' NONE ("", [])
+      ((map (fn t => (("", []), [(t, [])])) o maps (mk_prop thy)) insts)
+  end;
 
 in
 
 val axclass_instance_arity =
   gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity;

     val (c, thy') = thy
       |> AxClass.define_class_i (name, supsort) params axs;
     val {intro, axioms, ...} = AxClass.get_definition thy' c;
   in ((c, (intro, axioms)), thy') end;
 
+(* FIXME proper locale interface *)
 fun prove_interpretation_i (prfx, atts) expr insts tac thy =
   let
-    fun ad_hoc_term NONE = NONE
-      | ad_hoc_term (SOME (Const (c, ty))) =
+    fun ad_hoc_term (Const (c, ty)) =
           let
             val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_typ thy))) ty;
             val s = c ^ "::" ^ Pretty.output p;
-          in SOME s end
-      | ad_hoc_term (SOME t) =
+          in s end
+      | ad_hoc_term t =
           let
             val p = setmp show_types true (setmp show_sorts true (setmp print_mode [] (Sign.pretty_term thy))) t;
             val s = Pretty.output p;
-          in SOME s end;
+          in s end;
   in
     thy
-    |> Locale.interpretation (prfx, atts) expr (map ad_hoc_term insts)
+    |> 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)
-    |-> (fn _ => I)
+    |> ProofContext.theory_of
   end;
 
 fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
   let
     val supclasses = map (prep_class thy) raw_supclasses;

 
 end; (* local *)
 
 local
 
-fun add_interpretation_in (after_qed : theory -> theory) (name, expr) thy =
+(* FIXME proper locale interface *)
+fun prove_interpretation_in tac after_qed (name, expr) thy =
   thy
-  |> Locale.interpretation_in_locale (name, expr);
-
-fun prove_interpretation_in tac (after_qed : theory -> theory) (name, expr) thy =
-  thy
-  |> Locale.interpretation_in_locale (name, expr)
+  |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
   |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
-  |> snd
-  |> after_qed;
+  |> ProofContext.theory_of;
 
 fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
   let
     val class = prep_class theory raw_class;
     val sort = prep_sort theory raw_sort;

     |> do_proof after_qed (loc_name, loc_expr)
   end;
 
 fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof;
 fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof;
-val setup_proof = add_interpretation_in;
+val setup_proof = Locale.interpretation_in_locale o ProofContext.theory;
 val tactic_proof = prove_interpretation_in;
 
 in
 
 val instance_sort = instance_sort' setup_proof;