common entity definitions within a global or local theory context;

--- a/src/Pure/Isar/attrib.ML	Thu May 12 14:38:53 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu May 12 22:06:18 2016 +0200
@@ -109,13 +109,9 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val get_attributes = Attributes.get o Context.Proof;
+val ops_attributes = {get_data = Attributes.get, put_data = Attributes.put};
 
-fun transfer_attributes ctxt =
-  let
-    val attribs0 = Attributes.get (Context.Theory (Proof_Context.theory_of ctxt));
-    val attribs' = Name_Space.merge_tables (attribs0, get_attributes ctxt);
-  in Context.proof_map (Attributes.put attribs') ctxt end;
+val get_attributes = Attributes.get o Context.Proof;
 
 fun print_attributes verbose ctxt =
   let
@@ -134,19 +130,11 @@
 
 (* define *)
 
-fun define_global binding att comment thy =
-  let
-    val context = Context.Theory thy;
-    val (name, attribs') =
-      Name_Space.define context true (binding, (att, comment)) (Attributes.get context);
-  in (name, Context.the_theory (Attributes.put attribs' context)) end;
+fun define_global binding att comment =
+  Entity.define_global ops_attributes binding (att, comment);
 
 fun define binding att comment =
-  Local_Theory.background_theory_result (define_global binding att comment)
-  #-> (fn name =>
-    Local_Theory.map_contexts (K transfer_attributes)
-    #> Local_Theory.generic_alias Attributes.map binding name
-    #> pair name);
+  Entity.define ops_attributes binding (att, comment);
 
 
 (* check *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/entity.ML	Thu May 12 22:06:18 2016 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/Isar/entity.ML
+    Author:     Makarius
+
+Entity definitions within a global or local theory context.
+*)
+
+signature ENTITY =
+sig
+  type 'a data_ops =
+   {get_data: Context.generic -> 'a Name_Space.table,
+    put_data: 'a Name_Space.table -> Context.generic -> Context.generic}
+  val define_global: 'a data_ops -> binding -> 'a -> theory -> string * theory
+  val define: 'a data_ops -> binding -> 'a -> local_theory -> string * local_theory
+end;
+
+structure Entity: ENTITY =
+struct
+
+(* context data *)
+
+type 'a data_ops =
+ {get_data: Context.generic -> 'a Name_Space.table,
+  put_data: 'a Name_Space.table -> Context.generic -> Context.generic};
+
+
+(* global definition (foundation) *)
+
+fun define_global {get_data, put_data} b x thy =
+  let
+    val context = Context.Theory thy;
+    val (name, data') = Name_Space.define context true (b, x) (get_data context);
+  in (name, Context.the_theory (put_data data' context)) end;
+
+
+(* local definition *)
+
+fun alias {get_data, put_data} binding name =
+  Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+    let
+      val naming = Name_Space.naming_of context;
+      val binding' = Morphism.binding phi binding;
+      val data' = Name_Space.alias_table naming binding' name (get_data context);
+    in put_data data' context end);
+
+fun transfer {get_data, put_data} ctxt =
+  let
+    val data0 = get_data (Context.Theory (Proof_Context.theory_of ctxt));
+    val data' = Name_Space.merge_tables (data0, get_data (Context.Proof ctxt));
+  in Context.proof_map (put_data data') ctxt end;
+
+fun define ops binding x =
+  Local_Theory.background_theory_result (define_global ops binding x)
+  #-> (fn name =>
+    Local_Theory.map_contexts (K (transfer ops))
+    #> alias ops binding name
+    #> pair name);
+
+end;

--- a/src/Pure/Isar/local_theory.ML	Thu May 12 14:38:53 2016 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu May 12 22:06:18 2016 +0200
@@ -61,9 +61,6 @@
   val set_defsort: sort -> local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val generic_alias:
-    (('a Name_Space.table -> 'a Name_Space.table) -> Context.generic -> Context.generic) ->
-    binding -> string -> local_theory -> local_theory
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
@@ -329,13 +326,6 @@
 
 (* name space aliases *)
 
-fun generic_alias app b name =
-  declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-    let
-      val naming = Name_Space.naming_of context;
-      val b' = Morphism.binding phi b;
-    in app (Name_Space.alias_table naming b' name) context end);
-
 fun syntax_alias global_alias local_alias b name =
   declaration {syntax = true, pervasive = false} (fn phi =>
     let val b' = Morphism.binding phi b

--- a/src/Pure/Isar/method.ML	Thu May 12 14:38:53 2016 +0200
+++ b/src/Pure/Isar/method.ML	Thu May 12 22:06:18 2016 +0200
@@ -333,6 +333,8 @@
 val get_methods = fst o Data.get;
 val map_methods = Data.map o apfst;
 
+val ops_methods = {get_data = get_methods, put_data = map_methods o K};
+
 
 (* ML tactic *)
 
@@ -390,12 +392,6 @@
 
 (* method definitions *)
 
-fun transfer_methods ctxt =
-  let
-    val meths0 = get_methods (Context.Theory (Proof_Context.theory_of ctxt));
-    val meths' = Name_Space.merge_tables (meths0, get_methods (Context.Proof ctxt));
-  in Context.proof_map (map_methods (K meths')) ctxt end;
-
 fun print_methods verbose ctxt =
   let
     val meths = get_methods (Context.Proof ctxt);
@@ -411,19 +407,11 @@
 
 (* define *)
 
-fun define_global binding meth comment thy =
-  let
-    val context = Context.Theory thy;
-    val (name, meths') =
-      Name_Space.define context true (binding, (meth, comment)) (get_methods context);
-  in (name, Context.the_theory (map_methods (K meths') context)) end;
+fun define_global binding meth comment =
+  Entity.define_global ops_methods binding (meth, comment);
 
 fun define binding meth comment =
-  Local_Theory.background_theory_result (define_global binding meth comment)
-  #-> (fn name =>
-    Local_Theory.map_contexts (K transfer_methods)
-    #> Local_Theory.generic_alias map_methods binding name
-    #> pair name);
+  Entity.define ops_methods binding (meth, comment);
 
 
 (* check *)

--- a/src/Pure/ROOT.ML	Thu May 12 14:38:53 2016 +0200
+++ b/src/Pure/ROOT.ML	Thu May 12 22:06:18 2016 +0200
@@ -204,6 +204,7 @@
 
 (*theory specifications*)
 ML_file "Isar/local_theory.ML";
+ML_file "Isar/entity.ML";
 ML_file "Thy/thy_header.ML";
 ML_file "PIDE/command_span.ML";
 ML_file "Thy/thy_syntax.ML";