# HG changeset patch
# User krauss
# Date 1335655045 -7200
# Node ID 2d48bf79b7256416a395e854b9883443cfbf3d23
# Parent  0e36cc70cb3ed3a1049c57abeaf571be18b6c7cd
dependency graphs: fixed direction of edges

diff -r 0e36cc70cb3e -r 2d48bf79b725 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sat Apr 28 18:09:50 2012 +0200
+++ b/src/HOL/Tools/Function/termination.ML	Sun Apr 29 01:17:25 2012 +0200
@@ -315,7 +315,7 @@
   |> fold (fn c => Term_Graph.new_node (c, ())) cs
   |> fold_product (fn c1 => fn c2 =>
      if is_none (get_chain D c1 c2 |> the_default NONE)
-     then Term_Graph.add_edge (c1, c2) else I)
+     then Term_Graph.add_edge (c2, c1) else I)
      cs cs
 
 fun ucomp_empty_tac T =