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