--- a/Nominal/nominal_function_common.ML	Mon Jul 18 10:50:21 2011 +0100
+++ b/Nominal/nominal_function_common.ML	Mon Jul 18 17:40:13 2011 +0100
@@ -7,11 +7,110 @@
 Redefinition of config datatype 
 *)
 
+signature NOMINAL_FUNCTION_DATA =
+sig
+
+type nominal_info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination: thm,
+  eqvts: thm list}
+
+end
 
 
 structure Nominal_Function_Common =
 struct
 
+type nominal_info =
+ {is_partial : bool,
+  defname : string,
+    (* contains no logical entities: invariant under morphisms: *)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Attrib.src list -> thm list -> local_theory -> thm list * local_theory,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination: thm,
+  eqvts: thm list}
+
+fun morph_function_data ({add_simps, case_names, fs, R, psimps, pinducts,
+  simps, inducts, termination, defname, is_partial, eqvts} : nominal_info) phi =
+    let
+      val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
+      val name = Binding.name_of o Morphism.binding phi o Binding.name
+    in
+      { add_simps = add_simps, case_names = case_names,
+        fs = map term fs, R = term R, psimps = fact psimps,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
+        defname = name defname, is_partial=is_partial, eqvts = (*fact*) eqvts }
+    end
+
+structure NominalFunctionData = Generic_Data
+(
+  type T = (term * nominal_info) Item_Net.T;
+  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
+  val extend = I;
+  fun merge tabs : T = Item_Net.merge tabs;
+)
+
+val get_function = NominalFunctionData.get o Context.Proof;
+
+
+fun lift_morphism thy f =
+  let
+    val term = Drule.term_rule thy f
+  in
+    Morphism.thm_morphism f $> Morphism.term_morphism term
+    $> Morphism.typ_morphism (Logic.type_map term)
+  end
+
+fun import_function_data t ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt
+    val ct = cterm_of thy t
+    val inst_morph = lift_morphism thy o Thm.instantiate
+
+    fun match (trm, data) =
+      SOME (morph_function_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
+      handle Pattern.MATCH => NONE
+  in
+    get_first match (Item_Net.retrieve (get_function ctxt) t)
+  end
+
+fun import_last_function ctxt =
+  case Item_Net.content (get_function ctxt) of
+    [] => NONE
+  | (t, data) :: _ =>
+    let
+      val ([t'], ctxt') = Variable.import_terms true [t] ctxt
+    in
+      import_function_data t' ctxt'
+    end
+
+val all_function_data = Item_Net.content o get_function
+
+fun add_function_data (data : nominal_info as {fs, termination, ...}) =
+  NominalFunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
+  #> Function_Common.store_termination_rule termination
+
+
+
 
 (* Configuration management *)
 datatype nominal_function_opt
@@ -48,4 +147,15 @@
   NominalFunctionConfig { sequential=false, default=NONE,
     domintros=false, partials=true, inv=NONE}
 
+datatype nominal_function_result = NominalFunctionResult of
+ {fs: term list,
+  G: term,
+  R: term,
+  psimps : thm list,
+  simple_pinducts : thm list,
+  cases : thm,
+  termination : thm,
+  domintros : thm list option,
+  eqvts : thm list}
+
 end