src/HOL/Tools/Function/termination.ML
changeset 33855 cd8acf137c9c
parent 33099 b8cdd3d73022
child 34228 bc0cea4cae52
     1.1 --- a/src/HOL/Tools/Function/termination.ML	Mon Nov 23 13:45:16 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/termination.ML	Mon Nov 23 15:05:59 2009 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
     1.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
     1.6        let
     1.7 -        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
     1.8 +        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
     1.9            = Term.strip_qnt_body "Ex" c
    1.10        in cons r o cons l end
    1.11    in
    1.12 @@ -181,7 +181,6 @@
    1.13  
    1.14  fun dest_call D (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    1.15    let
    1.16 -    val n = get_num_points D
    1.17      val (sk, _, _, _, _) = D
    1.18      val vs = Term.strip_qnt_vars "Ex" c
    1.19  
    1.20 @@ -196,7 +195,7 @@
    1.21    | dest_call D t = error "dest_call"
    1.22  
    1.23  
    1.24 -fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
    1.25 +fun derive_desc_aux thy tac c (vs, _, l', _, r', Gam) m1 m2 D =
    1.26    case get_descent D c m1 m2 of
    1.27      SOME _ => D
    1.28    | NONE => let
    1.29 @@ -225,7 +224,7 @@
    1.30  
    1.31  (* all descents in one go *)
    1.32  fun derive_descents thy tac c D =
    1.33 -  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
    1.34 +  let val cdesc as (_, p, _, q, _, _) = dest_call D c
    1.35    in fold_product (derive_desc_aux thy tac c cdesc)
    1.36         (get_measures D p) (get_measures D q) D
    1.37    end
    1.38 @@ -280,7 +279,7 @@
    1.39      let
    1.40        val thy = ProofContext.theory_of ctxt
    1.41        val cert = cterm_of (theory_of_thm st)
    1.42 -      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
    1.43 +      val ((_ $ (_ $ rel)) :: ineqs) = prems_of st
    1.44  
    1.45        fun mk_compr ineq =
    1.46            let