--- 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
--- 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
--- 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;