# HG changeset patch
# User wenzelm
# Date 1441366760 -7200
# Node ID e966c311e9a78a7aab560074b960fd389d8f0208
# Parent  2618e7e3b5ea69e69a1421c640741fa0ab3f7ae3
trim context for persistent storage;
tuned signature;

diff -r 2618e7e3b5ea -r e966c311e9a7 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri Sep 04 11:38:35 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri Sep 04 13:39:20 2015 +0200
@@ -273,8 +273,7 @@
     val cong = #case_cong (Old_Datatype_Data.the_info thy n)
       |> safe_mk_meta_eq
   in
-    Context.theory_map
-      (Function_Context_Tree.map_function_congs (Thm.add_thm cong)) thy
+    Context.theory_map (Function_Context_Tree.add_function_cong cong) thy
   end
 
 val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_case_cong)))
diff -r 2618e7e3b5ea -r e966c311e9a7 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 11:38:35 2015 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Fri Sep 04 13:39:20 2015 +0200
@@ -282,7 +282,7 @@
 
 fun termination_rule_tac ctxt = resolve_tac ctxt (#1 (Data.get (Context.Proof ctxt)))
 
-val store_termination_rule = Data.map o @{apply 4(1)} o cons
+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, ...}) =
diff -r 2618e7e3b5ea -r e966c311e9a7 src/HOL/Tools/Function/function_context_tree.ML
--- a/src/HOL/Tools/Function/function_context_tree.ML	Fri Sep 04 11:38:35 2015 +0200
+++ b/src/HOL/Tools/Function/function_context_tree.ML	Fri Sep 04 13:39:20 2015 +0200
@@ -10,10 +10,8 @@
   type ctxt = (string * typ) list * thm list
   type ctx_tree
 
-  (* FIXME: This interface is a mess and needs to be cleaned up! *)
   val get_function_congs : Proof.context -> thm list
   val add_function_cong : thm -> Context.generic -> Context.generic
-  val map_function_congs : (thm list -> thm list) -> Context.generic -> Context.generic
 
   val cong_add: attribute
   val cong_del: attribute
@@ -53,14 +51,17 @@
   val merge = Thm.merge_thms
 );
 
-val get_function_congs = FunctionCongs.get o Context.Proof
-val map_function_congs = FunctionCongs.map
-val add_function_cong = FunctionCongs.map o Thm.add_thm
+fun get_function_congs ctxt =
+  FunctionCongs.get (Context.Proof ctxt)
+  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
+
+val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;
+
 
 (* congruence rules *)
 
-val cong_add = Thm.declaration_attribute (map_function_congs o Thm.add_thm o safe_mk_meta_eq);
-val cong_del = Thm.declaration_attribute (map_function_congs o Thm.del_thm o safe_mk_meta_eq);
+val cong_add = Thm.declaration_attribute (add_function_cong o safe_mk_meta_eq);
+val cong_del = Thm.declaration_attribute (FunctionCongs.map o Thm.del_thm o safe_mk_meta_eq);
 
 
 type depgraph = int Int_Graph.T