# HG changeset patch
# User wenzelm
# Date 1248627431 -7200
# Node ID 443d5cfaba1b7d6e51b2b9a984c976c1736a01ef
# Parent  3689b647356d3fca8bc0dda94321639823931235
SUBPROOF/Obtain.result: named params;

diff -r 3689b647356d -r 443d5cfaba1b src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 13:21:12 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Jul 26 18:57:11 2009 +0200
@@ -1257,7 +1257,7 @@
             [resolve_tac exists_fresh' 1,
              simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms @
                fin_set_supp @ ths)) 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -1324,7 +1324,7 @@
                        val _ $ (_ $ _ $ u) = concl';
                        val U = fastype_of u;
                        val (xs, params') =
-                         chop (length cargs) (map term_of params);
+                         chop (length cargs) (map (term_of o #2) params);
                        val Ts = map fastype_of xs;
                        val cnstr = Const (cname, Ts ---> U);
                        val (pis, z) = split_last params';
@@ -1640,7 +1640,7 @@
                     REPEAT_DETERM (resolve_tac [allI, impI] 1),
                     REPEAT_DETERM (etac conjE 1),
                     rtac unique 1,
-                    SUBPROOF (fn {prems = prems', params = [a, b], ...} => EVERY
+                    SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY
                       [cut_facts_tac [rec_prem] 1,
                        rtac (Thm.instantiate ([],
                          [(cterm_of thy11 (Var (("pi", 0), mk_permT aT)),
@@ -1693,7 +1693,7 @@
              REPEAT_DETERM (dresolve_tac (the (AList.lookup op = rec_fin_supp T)) 1),
              resolve_tac exists_fresh' 1,
              asm_simp_tac (HOL_ss addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -1763,7 +1763,7 @@
                     val cargsr' = partition_cargs idxs cargsr;
                     val boundsr = List.concat (map fst cargsr');
                     val (params1, _ :: params2) =
-                      chop (length params div 2) (map term_of params);
+                      chop (length params div 2) (map (term_of o #2) params);
                     val params' = params1 @ params2;
                     val rec_prems = filter (fn th => case prop_of th of
                         _ $ p => (case head_of p of
diff -r 3689b647356d -r 443d5cfaba1b src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 13:21:12 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Jul 26 18:57:11 2009 +0200
@@ -301,7 +301,7 @@
           (fn _ => EVERY
             [resolve_tac exists_fresh' 1,
              resolve_tac fs_atoms 1]);
-        val (([cx], ths), ctxt') = Obtain.result
+        val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [etac exE 1,
              full_simp_tac (HOL_ss addsimps (fresh_prod :: fresh_atm)) 1,
@@ -319,7 +319,7 @@
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
                let
                  val (params', (pis, z)) =
-                   chop (length params - length atomTs - 1) (map term_of params) ||>
+                   chop (length params - length atomTs - 1) (map (term_of o #2) params) ||>
                    split_last;
                  val bvars' = map
                    (fn (Bound i, T) => (nth params' (length params' - i), T)
@@ -474,7 +474,7 @@
                 rtac (first_order_mrs case_hyps case_hyp) 1
               else
                 let
-                  val params' = map (term_of o nth (rev params)) is;
+                  val params' = map (term_of o #2 o nth (rev params)) is;
                   val tab = params' ~~ map fst qs;
                   val (hyps1, hyps2) = chop (length args) case_hyps;
                   (* turns a = t and [x1 # t, ..., xn # t] *)
@@ -635,7 +635,7 @@
             val prems'' = map (fn th => Simplifier.simplify eqvt_ss
               (mk_perm_bool (cterm_of thy pi) th)) prems';
             val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
-               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of) params)
+               map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
                intr
           in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
           end) ctxt' 1 st
diff -r 3689b647356d -r 443d5cfaba1b src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 13:21:12 2009 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Jul 26 18:57:11 2009 +0200
@@ -323,7 +323,7 @@
         val avoid_th = Drule.instantiate'
           [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
           ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
-        val (([cx], th1 :: th2 :: ths), ctxt') = Obtain.result
+        val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
           (fn _ => EVERY
             [rtac avoid_th 1,
              full_simp_tac (HOL_ss addsimps [@{thm fresh_star_prod_set}]) 1,
@@ -359,7 +359,7 @@
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>
                let
                  val (cparams', (pis, z)) =
-                   chop (length params - length atomTs - 1) params ||>
+                   chop (length params - length atomTs - 1) (map #2 params) ||>
                    (map term_of #> split_last);
                  val params' = map term_of cparams'
                  val sets' = map (apfst (curry subst_bounds (rev params'))) sets;