# HG changeset patch
# User wenzelm
# Date 1518813184 -3600
# Node ID 9225bb0d132708d504d44a9f5cf330e3e04e5f25
# Parent  9a1212f4393e4692a79a57b55c3c95297ad5fa48
trim context of persistent data;
tuned signature;

diff -r 9a1212f4393e -r 9225bb0d1327 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Feb 16 20:44:25 2018 +0100
+++ b/src/HOL/Tools/Function/function.ML	Fri Feb 16 21:33:04 2018 +0100
@@ -6,15 +6,13 @@
 
 signature FUNCTION =
 sig
-  include FUNCTION_DATA
-
   val add_function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> local_theory -> Function_Common.info * local_theory
 
   val add_function_cmd: (binding * string option * mixfix) list ->
     Specification.multi_specs_cmd -> Function_Common.function_config ->
-    (Proof.context -> tactic) -> bool -> local_theory -> info * local_theory
+    (Proof.context -> tactic) -> bool -> local_theory -> Function_Common.info * local_theory
 
   val function: (binding * typ option * mixfix) list ->
     Specification.multi_specs -> Function_Common.function_config ->
@@ -25,16 +23,16 @@
     bool -> local_theory -> Proof.state
 
   val prove_termination: term option -> tactic -> local_theory ->
-    info * local_theory
+    Function_Common.info * local_theory
   val prove_termination_cmd: string option -> tactic -> local_theory ->
-    info * local_theory
+    Function_Common.info * local_theory
 
   val termination : term option -> local_theory -> Proof.state
   val termination_cmd : string option -> local_theory -> Proof.state
 
   val get_congs : Proof.context -> thm list
 
-  val get_info : Proof.context -> term -> info
+  val get_info : Proof.context -> term -> Function_Common.info
 end
 
 
@@ -266,7 +264,7 @@
 
 val get_congs = Function_Context_Tree.get_function_congs
 
-fun get_info ctxt t = Item_Net.retrieve (get_functions ctxt) t
+fun get_info ctxt t = Function_Common.retrieve_function_data ctxt t
   |> the_single |> snd
 
 
diff -r 9a1212f4393e -r 9225bb0d1327 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Feb 16 20:44:25 2018 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Feb 16 21:33:04 2018 +0100
@@ -4,7 +4,7 @@
 Common definitions and other infrastructure for the function package.
 *)
 
-signature FUNCTION_DATA =
+signature FUNCTION_COMMON =
 sig
   type info =
    {is_partial : bool,
@@ -26,37 +26,6 @@
     cases : thm list,
     pelims: thm list list,
     elims: thm list list option}
-end
-
-structure Function_Data : FUNCTION_DATA =
-struct
-
-type info =
- {is_partial : bool,
-  defname : binding,
-    (*contains no logical entities: invariant under morphisms:*)
-  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
-    Token.src list -> thm list -> local_theory -> thm list * local_theory,
-  fnames : binding list,
-  case_names : string list,
-  fs : term list,
-  R : term,
-  dom: term,
-  psimps: thm list,
-  pinducts: thm list,
-  simps : thm list option,
-  inducts : thm list option,
-  termination : thm,
-  totality : thm option,
-  cases : thm list,
-  pelims : thm list list,
-  elims : thm list list option}
-
-end
-
-signature FUNCTION_COMMON =
-sig
-  include FUNCTION_DATA
   val profile : bool Unsynchronized.ref
   val PROFILE : string -> ('a -> 'b) -> 'a -> 'b
   val mk_acc : typ -> term -> term
@@ -78,7 +47,7 @@
     preproc
   val termination_rule_tac : Proof.context -> int -> tactic
   val store_termination_rule : thm -> Context.generic -> Context.generic
-  val get_functions : Proof.context -> (term * info) Item_Net.T
+  val retrieve_function_data : Proof.context -> term -> (term * info) list
   val add_function_data : info -> Context.generic -> Context.generic
   val termination_prover_tac : bool -> Proof.context -> tactic
   val set_termination_prover : (bool -> Proof.context -> tactic) -> Context.generic ->
@@ -107,9 +76,46 @@
 structure Function_Common : FUNCTION_COMMON =
 struct
 
-open Function_Data
+local open Function_Lib in
+
+(* info *)
 
-local open Function_Lib in
+type info =
+ {is_partial : bool,
+  defname : binding,
+    (*contains no logical entities: invariant under morphisms:*)
+  add_simps : (binding -> binding) -> string -> (binding -> binding) ->
+    Token.src list -> thm list -> local_theory -> thm list * local_theory,
+  fnames : binding list,
+  case_names : string list,
+  fs : term list,
+  R : term,
+  dom: term,
+  psimps: thm list,
+  pinducts: thm list,
+  simps : thm list option,
+  inducts : thm list option,
+  termination : thm,
+  totality : thm option,
+  cases : thm list,
+  pelims : thm list list,
+  elims : thm list list option}
+
+fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
+  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
+    let
+      val term = Morphism.term phi
+      val thm = Morphism.thm phi
+      val fact = Morphism.fact phi
+    in
+      { add_simps = add_simps, case_names = case_names, fnames = fnames,
+        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
+        pinducts = fact pinducts, simps = Option.map fact simps,
+        inducts = Option.map fact inducts, termination = thm termination,
+        totality = Option.map thm totality, defname = Morphism.binding phi defname,
+        is_partial = is_partial, cases = fact cases,
+        elims = Option.map (map fact) elims, pelims = map fact pelims }
+    end
 
 
 (* profiling *)
@@ -267,9 +273,17 @@
 val store_termination_rule = Data.map o @{apply 4(1)} o cons o Thm.trim_context
 
 val get_functions = #2 o Data.get o Context.Proof
-fun add_function_data (info : info as {fs, termination, ...}) =
-  (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
-  #> store_termination_rule termination
+
+fun retrieve_function_data ctxt t =
+  Item_Net.retrieve (get_functions ctxt) t
+  |> (map o apsnd)
+      (transform_function_data (Morphism.transfer_morphism (Proof_Context.theory_of ctxt)));
+
+val add_function_data =
+  transform_function_data Morphism.trim_context_morphism #>
+  (fn info as {fs, termination, ...} =>
+    (Data.map o @{apply 4(2)}) (fold (fn f => Item_Net.update (f, info)) fs)
+    #> store_termination_rule termination)
 
 fun termination_prover_tac quiet ctxt = #3 (Data.get (Context.Proof ctxt)) quiet ctxt
 val set_termination_prover = Data.map o @{apply 4(3)} o K
@@ -292,22 +306,6 @@
   termination : thm,
   domintros : thm list option}
 
-fun transform_function_data phi ({add_simps, case_names, fnames, fs, R, dom, psimps, pinducts,
-  simps, inducts, termination, totality, defname, is_partial, cases, pelims, elims} : info) =
-    let
-      val term = Morphism.term phi
-      val thm = Morphism.thm phi
-      val fact = Morphism.fact phi
-    in
-      { add_simps = add_simps, case_names = case_names, fnames = fnames,
-        fs = map term fs, R = term R, dom = term dom, psimps = fact psimps,
-        pinducts = fact pinducts, simps = Option.map fact simps,
-        inducts = Option.map fact inducts, termination = thm termination,
-        totality = Option.map thm totality, defname = Morphism.binding phi defname,
-        is_partial = is_partial, cases = fact cases,
-        elims = Option.map (map fact) elims, pelims = map fact pelims }
-    end
-
 fun lift_morphism ctxt f =
   let
     fun term t = Thm.term_of (Drule.cterm_rule f (Thm.cterm_of ctxt t))
@@ -328,7 +326,7 @@
       SOME (transform_function_data (inst_morph (Thm.match (Thm.cterm_of ctxt trm, ct))) data)
         handle Pattern.MATCH => NONE
   in
-    get_first match (Item_Net.retrieve (get_functions ctxt) t)
+    get_first match (retrieve_function_data ctxt t)
   end
 
 fun import_last_function ctxt =