# HG changeset patch
# User wenzelm
# Date 1535631700 -7200
# Node ID d36f00510e40e13ce9fdd027dd4134e4391e2ce0
# Parent  becaeaa334aef3a887186f9ddc066ad45d4f93cf
tuned signature;

diff -r becaeaa334ae -r d36f00510e40 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Thu Aug 30 14:10:39 2018 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Thu Aug 30 14:21:40 2018 +0200
@@ -328,10 +328,10 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, some_axiom, some_assm_intro, of_class) =>
-       Context.theory_map (Locale.add_registration
+       Locale.add_registration_theory
          {dep = (class, base_morph),
            mixin = Option.map (rpair true) eq_morph,
-           export = export_morph})
+           export = export_morph}
     #> Class.register class sups params base_sort base_morph export_morph some_axiom some_assm_intro of_class
     #> Global_Theory.store_thm (prefix (Binding.qualified_name (class ^ ".of_class.intro")), of_class)))
     |> snd
diff -r becaeaa334ae -r d36f00510e40 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:10:39 2018 +0200
+++ b/src/Pure/Isar/generic_target.ML	Thu Aug 30 14:21:40 2018 +0200
@@ -370,7 +370,7 @@
   background_declaration decl #> standard_declaration (K true) decl;
 
 val theory_registration =
-  Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
+  Local_Theory.raw_theory o Locale.add_registration_theory;
 
 
 
diff -r becaeaa334ae -r d36f00510e40 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Aug 30 14:10:39 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 30 14:21:40 2018 +0200
@@ -76,6 +76,7 @@
   type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
   val amend_registration: registration -> Context.generic -> Context.generic
   val add_registration: registration -> Context.generic -> Context.generic
+  val add_registration_theory: registration -> theory -> theory
   val add_registration_proof: registration -> Proof.context -> Proof.context
   val add_registration_local_theory: registration -> local_theory -> local_theory
   val activate_fragment: registration -> local_theory -> local_theory
@@ -559,12 +560,13 @@
       |> activate_facts (SOME export) (name, morph)
   end;
 
+val add_registration_theory = Context.theory_map o add_registration;
+
 fun add_registration_proof registration ctxt = ctxt
   |> Proof_Context.set_stmt false
   |> Context.proof_map (add_registration registration)
   |> Proof_Context.restore_stmt ctxt;
 
-
 fun add_registration_local_theory registration lthy =
   let val n = Local_Theory.level lthy in
     lthy |> Local_Theory.map_contexts (fn level =>
@@ -607,8 +609,10 @@
     val (_, regs) =
       fold_rev (roundup thy' cons export)
         (registrations_of context' loc) (Idents.get context', []);
-    fun add_dep dep = add_registration {dep = dep, mixin = NONE, export = export};
-  in thy' |> fold_rev (Context.theory_map o add_dep) regs end;
+  in
+    thy'
+    |> fold_rev (fn dep => add_registration_theory {dep = dep, mixin = NONE, export = export}) regs
+  end;
 
 
 (*** Storing results ***)