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.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.20 @@ -196,7 +195,7 @@
1.21    | dest_call D t = error "dest_call"
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.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.45        fun mk_compr ineq =
1.46            let