# HG changeset patch
# User wenzelm
# Date 1146859183 -7200
# Node ID 2d9940cd52d3edfe69bafe2d86f5d870479596ea
# Parent  7c761751e9986cf10208114fd90dd32bc13d9057
replaced Graph.find_paths by Graph.irreducible_paths;

diff -r 7c761751e998 -r 2d9940cd52d3 src/HOL/Tools/recfun_codegen.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
diff -r 7c761751e998 -r 2d9940cd52d3 src/Pure/Tools/class_package.ML
--- 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;