changeset 47835 | 2d48bf79b725 |
parent 47433 | 07f4bf913230 |
child 52723 | 2ebcc81f599c |
--- 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 =