src/HOL/Tools/Function/termination.ML

 fun mk_dgraph D cs =
   Term_Graph.empty
   |> 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 =
   REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
     ORELSE' rtac @{thm union_comp_emptyL}