src/HOL/Nominal/nominal_inductive.ML
changeset 32202 443d5cfaba1b
parent 32172 c4e55f30d527
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 13:21:12 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 18:57:11 2009 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4            (fn _ => EVERY
     1.5              [resolve_tac exists_fresh' 1,
     1.6               resolve_tac fs_atoms 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 @@ -319,7 +319,7 @@
    1.13               SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
    1.14                 let
    1.15                   val (params', (pis, z)) =
    1.16 -                   chop (length params - length atomTs - 1) (map term_of params) ||>
    1.17 +                   chop (length params - length atomTs - 1) (map (term_of o #2) params) ||>
    1.18                     split_last;
    1.19                   val bvars' = map
    1.20                     (fn (Bound i, T) => (nth params' (length params' - i), T)
    1.21 @@ -474,7 +474,7 @@
    1.22                  rtac (first_order_mrs case_hyps case_hyp) 1
    1.23                else
    1.24                  let
    1.25 -                  val params' = map (term_of o nth (rev params)) is;
    1.26 +                  val params' = map (term_of o #2 o nth (rev params)) is;
    1.27                    val tab = params' ~~ map fst qs;
    1.28                    val (hyps1, hyps2) = chop (length args) case_hyps;
    1.29                    (* turns a = t and [x1 # t, ..., xn # t] *)
    1.30 @@ -635,7 +635,7 @@
    1.31              val prems'' = map (fn th => Simplifier.simplify eqvt_ss
    1.32                (mk_perm_bool (cterm_of thy pi) th)) prems';
    1.33              val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
    1.34 -               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
    1.35 +               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
    1.36                 intr
    1.37            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
    1.38            end) ctxt' 1 st