use IntGraph from Pure;
authorwenzelm
Thu, 11 May 2006 19:15:12 +0200
changeset 19612 1e133047809a
parent 19611 da2a0014c461
child 19613 9bf274ec94cf
use IntGraph from Pure;
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/function_package/fundef_common.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
--- 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