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