src/HOL/Tools/Function/termination.ML
changeset 32135 f645b51e8e54
parent 31971 8c1b845ed105
child 32149 ef59550a55d3
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Wed Jul 22 14:20:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Wed Jul 22 14:20:32 2009 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4  
     1.5  fun mk_sum_skel rel =
     1.6    let
     1.7 -    val cs = FundefLib.dest_binop_list @{const_name Un} rel
     1.8 +    val cs = FundefLib.dest_binop_list @{const_name union} rel
     1.9      fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
    1.10        let
    1.11          val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
    1.12 @@ -233,7 +233,7 @@
    1.13  fun CALLS tac i st =
    1.14    if Thm.no_prems st then all_tac st
    1.15    else case Thm.term_of (Thm.cprem_of st i) of
    1.16 -    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name Un} rel, i) st
    1.17 +    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name union} rel, i) st
    1.18    |_ => no_tac st
    1.19  
    1.20  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
    1.21 @@ -293,7 +293,7 @@
    1.22            if null ineqs then
    1.23                Const (@{const_name Set.empty}, fastype_of rel)
    1.24            else
    1.25 -              foldr1 (HOLogic.mk_binop @{const_name Un}) (map mk_compr ineqs)
    1.26 +              foldr1 (HOLogic.mk_binop @{const_name union}) (map mk_compr ineqs)
    1.27  
    1.28        fun solve_membership_tac i =
    1.29            (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)