replaced Graph.find_paths by Graph.irreducible_paths;
authorwenzelm
Fri, 05 May 2006 21:59:43 +0200
changeset 19575 2d9940cd52d3
parent 19574 7c761751e998
child 19576 179ad0076f75
replaced Graph.find_paths by Graph.irreducible_paths;
src/HOL/Tools/recfun_codegen.ML
src/Pure/Tools/class_package.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Fri May 05 21:59:43 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Fri May 05 21:59:43 2006 +0200
@@ -104,7 +104,7 @@
 
 fun cycle g (xs, x) =
   if x mem xs then xs
-  else Library.foldl (cycle g) (x :: xs, List.concat (Graph.find_paths (fst g) (x, x)));
+  else Library.foldl (cycle g) (x :: xs, List.concat (Graph.irreducible_paths (fst g) (x, x)));
 
 fun add_rec_funs thy defs gr dep eqs module =
   let
--- a/src/Pure/Tools/class_package.ML	Fri May 05 21:59:43 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Fri May 05 21:59:43 2006 +0200
@@ -162,7 +162,7 @@
 fun get_superclass_derivation thy (subclass, superclass) =
   if subclass = superclass
     then SOME [subclass]
-    else case Graph.find_paths ((fst o fst o ClassData.get) thy) (subclass, superclass)
+    else case Graph.irreducible_paths ((fst o fst o ClassData.get) thy) (subclass, superclass)
       of [] => NONE
        | (p::_) => (SOME o filter (is_operational_class thy)) p;