changeset 47433 | 07f4bf913230 |
parent 46218 | ecf6375e2abb |
child 47835 | 2d48bf79b725 |
--- a/src/HOL/Tools/Function/termination.ML Tue Apr 03 08:55:06 2012 +0200 +++ b/src/HOL/Tools/Function/termination.ML Tue Apr 03 17:26:30 2012 +0900 @@ -141,7 +141,7 @@ fun prove_chain thy chain_tac (c1, c2) = let val goal = - HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2), + HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.relcomp} (c1, c2), Const (@{const_abbrev Set.empty}, fastype_of c1)) |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *) in