diff -r cfe8d4bf749a -r 2040846d1bbe src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Mon Jul 16 21:17:12 2007 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Mon Jul 16 21:22:43 2007 +0200
@@ -9,19 +9,19 @@
 
 signature FUNDEF_CTXTREE =
 sig
+    type depgraph
     type ctx_tree
 
     (* FIXME: This interface is a mess and needs to be cleaned up! *)
     val cong_deps : thm -> int IntGraph.T
     val add_congs : thm list
 
-    val mk_tree: (thm * FundefCommon.depgraph) list ->
-                 (string * typ) -> term -> Proof.context -> term -> FundefCommon.ctx_tree
+    val mk_tree: (thm * depgraph) list ->
+                 (string * typ) -> term -> Proof.context -> term -> ctx_tree
 
-    val inst_tree: theory -> term -> term -> FundefCommon.ctx_tree
-                   -> FundefCommon.ctx_tree
+    val inst_tree: theory -> term -> term -> ctx_tree -> ctx_tree
 
-    val add_context_varnames : FundefCommon.ctx_tree -> string list -> string list
+    val add_context_varnames : ctx_tree -> string list -> string list
 
     val export_term : (string * typ) list * term list -> term -> term
     val export_thm : theory -> (string * typ) list * term list -> thm -> thm
@@ -33,9 +33,9 @@
    (((string * typ) list * thm list) * thm) list ->
    (((string * typ) list * thm list) * thm) list * 'b ->
    (((string * typ) list * thm list) * thm) list * 'b)
-   -> FundefCommon.ctx_tree -> 'b -> 'b
+   -> ctx_tree -> 'b -> 'b
 
-    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> FundefCommon.ctx_tree -> thm * (thm * thm) list
+    val rewrite_by_tree : theory -> term -> thm -> (thm * thm) list -> ctx_tree -> thm * (thm * thm) list
 end
 
 structure FundefCtxTree : FUNDEF_CTXTREE =
@@ -44,6 +44,13 @@
 open FundefCommon
 open FundefLib
 
+type depgraph = int IntGraph.T
+
+datatype ctx_tree 
+  = Leaf of term
+  | Cong of (term * thm * depgraph * ((string * typ) list * thm list * ctx_tree) list)
+  | RCall of (term * ctx_tree)
+
 
 (* Maps "Trueprop A = B" to "A" *)
 val rhs_of = snd o HOLogic.dest_eq o HOLogic.dest_Trueprop
@@ -160,7 +167,7 @@
 
 fun import_thm thy (fixes, athms) =
     fold (forall_elim o cterm_of thy o Free) fixes
- #> fold implies_elim_swp athms
+ #> fold (flip implies_elim) athms
 
 fun assume_in_ctxt thy (fixes, athms) prop =
     let