# HG changeset patch
# User wenzelm
# Date 1236955805 -3600
# Node ID cb7e886e4b1071aa0a521858f2ffc69e61eb6e7f
# Parent  772e9528045691cc448ff457ce5e562ead2c38b6
get data from plain Proof.context;

diff -r 772e95280456 -r cb7e886e4b10 src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Thu Mar 12 23:12:53 2009 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML	Fri Mar 13 15:50:05 2009 +0100
@@ -11,7 +11,7 @@
     type ctx_tree
 
     (* FIXME: This interface is a mess and needs to be cleaned up! *)
-    val get_fundef_congs : Context.generic -> thm list
+    val get_fundef_congs : Proof.context -> thm list
     val add_fundef_cong : thm -> Context.generic -> Context.generic
     val map_fundef_congs : (thm list -> thm list) -> Context.generic -> Context.generic
 
@@ -52,8 +52,8 @@
   fun merge _ = Thm.merge_thms
 );
 
-val map_fundef_congs = FundefCongs.map 
-val get_fundef_congs = FundefCongs.get
+val get_fundef_congs = FundefCongs.get o Context.Proof
+val map_fundef_congs = FundefCongs.map
 val add_fundef_cong = FundefCongs.map o Thm.add_thm
 
 (* congruence rules *)
@@ -127,7 +127,7 @@
 
 fun mk_tree fvar h ctxt t =
     let 
-      val congs = get_fundef_congs (Context.Proof ctxt)
+      val congs = get_fundef_congs ctxt
       val congs_deps = map (fn c => (c, cong_deps c)) (congs @ default_congs) (* FIXME: Save in theory *)
 
       fun matchcall (a $ b) = if a = Free fvar then SOME b else NONE
diff -r 772e95280456 -r cb7e886e4b10 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu Mar 12 23:12:53 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Mar 13 15:50:05 2009 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/function_package/fundef_common.ML
-    ID:         $Id$
     Author:     Alexander Krauss, TU Muenchen
 
 A package for general recursive function definitions. 
@@ -101,6 +100,8 @@
   fun merge _ (tab1, tab2) = NetRules.merge (tab1, tab2)
 );
 
+val get_fundef = FundefData.get o Context.Proof;
+
 
 (* Generally useful?? *)
 fun lift_morphism thy f = 
@@ -113,7 +114,7 @@
 
 fun import_fundef_data t ctxt =
     let
-      val thy = Context.theory_of ctxt
+      val thy = ProofContext.theory_of ctxt
       val ct = cterm_of thy t
       val inst_morph = lift_morphism thy o Thm.instantiate 
 
@@ -121,20 +122,20 @@
           SOME (morph_fundef_data data (inst_morph (Thm.match (cterm_of thy trm, ct))))
           handle Pattern.MATCH => NONE
     in 
-      get_first match (NetRules.retrieve (FundefData.get ctxt) t)
+      get_first match (NetRules.retrieve (get_fundef ctxt) t)
     end
 
 fun import_last_fundef ctxt =
-    case NetRules.rules (FundefData.get ctxt) of
+    case NetRules.rules (get_fundef ctxt) of
       [] => NONE
     | (t, data) :: _ =>
       let 
-        val ([t'], ctxt') = Variable.import_terms true [t] (Context.proof_of ctxt)
+        val ([t'], ctxt') = Variable.import_terms true [t] ctxt
       in
-        import_fundef_data t' (Context.Proof ctxt')
+        import_fundef_data t' ctxt'
       end
 
-val all_fundef_data = NetRules.rules o FundefData.get
+val all_fundef_data = NetRules.rules o get_fundef
 
 fun add_fundef_data (data as FundefCtxData {fs, termination, ...}) =
     FundefData.map (fold (fn f => NetRules.insert (f, data)) fs)
@@ -161,7 +162,7 @@
 );
 
 val set_termination_prover = TerminationProver.put
-val get_termination_prover = TerminationProver.get
+val get_termination_prover = TerminationProver.get o Context.Proof
 
 
 (* Configuration management *)