# HG changeset patch
# User wenzelm
# Date 1147367712 -7200
# Node ID 1e133047809a5cfbdccecd119101ad31d8a78ab7
# Parent  da2a0014c461c4b934760dad20290d387131260f
use IntGraph from Pure;

diff -r da2a0014c461 -r 1e133047809a src/HOL/Tools/function_package/context_tree.ML
--- a/src/HOL/Tools/function_package/context_tree.ML	Thu May 11 15:46:40 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML	Thu May 11 19:15:12 2006 +0200
@@ -12,7 +12,7 @@
     type ctx_tree
 
     (* FIXME: This interface is a mess and needs to be cleaned up! *)
-    val cong_deps : thm -> int FundefCommon.IntGraph.T
+    val cong_deps : thm -> int IntGraph.T
     val add_congs : thm list
 
     val mk_tree: theory -> (thm * FundefCommon.depgraph) list -> term -> term -> FundefCommon.ctx_tree
@@ -237,4 +237,4 @@
 	rewrite_help [] [] [] x tr
     end
 
-end
\ No newline at end of file
+end
diff -r da2a0014c461 -r 1e133047809a src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 15:46:40 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Thu May 11 19:15:12 2006 +0200
@@ -14,9 +14,6 @@
 
 
 
-(* Partial orders to represent dependencies *)
-structure IntGraph = GraphFun(type key = int val ord = int_ord);
-
 type depgraph = int IntGraph.T