--- 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
--- 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