src/HOL/Tools/function_package/context_tree.ML

 sig
     type ctxt = (string * typ) list * thm list (* poor man's contexts: fixes + assumes *)
     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
 
     val cong_add: attribute
     val cong_del: attribute

   val empty = []
   val extend = I
   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 *)
 
 val cong_add = Thm.declaration_attribute (map_fundef_congs o Thm.add_thm o safe_mk_meta_eq);

   | find_cong_rule _ _ _ [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
 
 
 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
         | matchcall _ = NONE