src/HOL/Nominal/nominal_datatype.ML
changeset 32202 443d5cfaba1b
parent 32172 c4e55f30d527
child 32715 becd87e4039b
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 13:21:12 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 18:57:11 2009 +0200
     1.3 @@ -1257,7 +1257,7 @@
     1.4              [resolve_tac exists_fresh' 1,
     1.5               simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
     1.6                 fin_set_supp @ ths)) 1]);
     1.7 -        val (([cx], ths), ctxt') = Obtain.result
     1.8 +        val (([(_, cx)], ths), ctxt') = Obtain.result
     1.9            (fn _ => EVERY
    1.10              [etac exE 1,
    1.11               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.12 @@ -1324,7 +1324,7 @@
    1.13                         val _ $ (_ $ _ $ u) = concl';
    1.14                         val U = fastype_of u;
    1.15                         val (xs, params') =
    1.16 -                         chop (length cargs) (map term_of params);
    1.17 +                         chop (length cargs) (map (term_of o #2) params);
    1.18                         val Ts = map fastype_of xs;
    1.19                         val cnstr = Const (cname, Ts ---> U);
    1.20                         val (pis, z) = split_last params';
    1.21 @@ -1640,7 +1640,7 @@
    1.22                      REPEAT_DETERM (resolve_tac [allI, impI] 1),
    1.23                      REPEAT_DETERM (etac conjE 1),
    1.24                      rtac unique 1,
    1.25 -                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
    1.26 +                    SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
    1.27                        [cut_facts_tac [rec_prem] 1,
    1.28                         rtac (Thm.instantiate ([],
    1.29                           [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
    1.30 @@ -1693,7 +1693,7 @@
    1.31               REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
    1.32               resolve_tac exists_fresh' 1,
    1.33               asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
    1.34 -        val (([cx], ths), ctxt') = Obtain.result
    1.35 +        val (([(_, cx)], ths), ctxt') = Obtain.result
    1.36            (fn _ => EVERY
    1.37              [etac exE 1,
    1.38               full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
    1.39 @@ -1763,7 +1763,7 @@
    1.40                      val cargsr' = partition_cargs idxs cargsr;
    1.41                      val boundsr = List.concat (map fst cargsr');
    1.42                      val (params1, _ :: params2) =
    1.43 -                      chop (length params div 2) (map term_of params);
    1.44 +                      chop (length params div 2) (map (term_of o #2) params);
    1.45                      val params' = params1 @ params2;
    1.46                      val rec_prems = filter (fn th => case prop_of th of
    1.47                          _ $ p => (case head_of p of