src/HOL/Tools/Function/termination.ML
changeset 35402 115a5a95710a
parent 35092 cfe605c54e50
child 35404 de56579ae229
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:56:03 2010 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Sat Feb 27 20:57:08 2010 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4  
     1.5      val relation =
     1.6        if null ineqs
     1.7 -      then Const (@{const_name Set.empty}, fastype_of rel)
     1.8 +      then Const (@{const_abbrev Set.empty}, fastype_of rel)
     1.9        else map mk_compr ineqs
    1.10          |> foldr1 (HOLogic.mk_binop @{const_name Lattices.sup})
    1.11  
    1.12 @@ -321,7 +321,7 @@
    1.13    let
    1.14      val goal =
    1.15        HOLogic.mk_eq (HOLogic.mk_binop @{const_name Relation.rel_comp} (c1, c2),
    1.16 -        Const (@{const_name Set.empty}, fastype_of c1))
    1.17 +        Const (@{const_abbrev Set.empty}, fastype_of c1))
    1.18        |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
    1.19    in
    1.20      case Function_Lib.try_proof (cterm_of thy goal) chain_tac of