# HG changeset patch # User wenzelm # Date 1437941954 -7200 # Node ID 722cb21ab680b5225768cec21639a64e5733a048 # Parent e3f2262786ea78d4ca2af2b8a7961ffec8e71c5e updated to infer_instantiate; diff -r e3f2262786ea -r 722cb21ab680 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Sun Jul 26 22:07:37 2015 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sun Jul 26 22:19:14 2015 +0200 @@ -22,8 +22,8 @@ (head_of (Logic.incr_indexes ([], Ts, j) t), fold_rev Term.abs ps u)) tinst; val th' = instf - (map (apply2 (Thm.ctyp_of ctxt)) tyinst') - (map (apply2 (Thm.cterm_of ctxt)) tinst') + (map (apsnd (Thm.ctyp_of ctxt)) tyinst') + (map (apsnd (Thm.cterm_of ctxt)) tinst') (Thm.lift_rule cgoal th) in compose_tac ctxt (elim, th', Thm.nprems_of th) i st @@ -33,11 +33,12 @@ fun res_inst_tac_term ctxt = gen_res_inst_tac_term ctxt (fn instT => fn inst => Thm.instantiate - (map (apfst (dest_TVar o Thm.typ_of)) instT, - map (apfst (dest_Var o Thm.term_of)) inst)); + (map (apfst dest_TVar) instT, + map (apfst dest_Var) inst)); fun res_inst_tac_term' ctxt = - gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) []; + gen_res_inst_tac_term ctxt + (fn _ => fn inst => infer_instantiate ctxt (map (apfst (#1 o dest_Var)) inst)) []; fun cut_inst_tac_term' ctxt tinst th = res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th); diff -r e3f2262786ea -r 722cb21ab680 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sun Jul 26 22:07:37 2015 +0200 +++ b/src/HOL/Nominal/nominal_primrec.ML Sun Jul 26 22:19:14 2015 +0200 @@ -281,7 +281,6 @@ val qualify = Binding.qualify false (space_implode "_" (map (Long_Name.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; - val cert = Thm.cterm_of lthy'; fun mk_idx eq = let @@ -305,16 +304,16 @@ (fold_rev (Term.add_vars o Logic.strip_assums_concl) (Thm.prems_of (hd rec_rewrites)) [])); val cfs = defs' |> hd |> snd |> strip_comb |> snd |> - curry (List.take o swap) (length fvars) |> map cert; + curry (List.take o swap) (length fvars) |> map (Thm.cterm_of lthy'); val invs' = (case invs of NONE => map (fn (i, _) => Abs ("x", fastype_of (snd (nth defs' i)), @{term True})) descr | SOME invs' => map (prep_term lthy') invs'); - val inst = (map cert fvars ~~ cfs) @ - (map (cert o Var) pvars ~~ map cert invs') @ + val inst = (map (#1 o dest_Var) fvars ~~ cfs) @ + (map #1 pvars ~~ map (Thm.cterm_of lthy') invs') @ (case ctxtvars of - [ctxtvar] => [(cert (Var ctxtvar), - cert (the_default HOLogic.unit (Option.map (prep_term lthy') fctxt)))] + [ctxtvar] => [(#1 ctxtvar, + Thm.cterm_of lthy' (the_default HOLogic.unit (Option.map (prep_term lthy') fctxt)))] | _ => []); val rec_rewrites' = map (fn eq => let @@ -324,24 +323,24 @@ HOLogic.dest_eq |> fst |> strip_comb |> snd |> List.last |> strip_comb |> snd in (cargs, Logic.strip_imp_prems eq, - Drule.cterm_instantiate (inst @ - (map cert cargs' ~~ map (cert o Free) cargs)) th) + infer_instantiate lthy' (inst @ + (map (#1 o dest_Var) cargs' ~~ map (Thm.cterm_of lthy' o Free) cargs)) th) end) eqns'; val prems = foldr1 (common_prefix op aconv) (map (Thm.prems_of o #3) rec_rewrites'); - val cprems = map cert prems; + val cprems = map (Thm.cterm_of lthy') prems; val asms = map Thm.assume cprems; val premss = map (fn (cargs, eprems, eqn) => map (fn t => fold_rev (Logic.all o Free) cargs (Logic.list_implies (eprems, t))) (List.drop (Thm.prems_of eqn, length prems))) rec_rewrites'; - val cpremss = map (map cert) premss; + val cpremss = map (map (Thm.cterm_of lthy')) premss; val asmss = map (map Thm.assume) cpremss; fun mk_eqn ((cargs, eprems, eqn), asms') = let - val ceprems = map cert eprems; + val ceprems = map (Thm.cterm_of lthy') eprems; val asms'' = map Thm.assume ceprems; - val ccargs = map (cert o Free) cargs; + val ccargs = map (Thm.cterm_of lthy' o Free) cargs; val asms''' = map (fn th => implies_elim_list (forall_elim_list ccargs th) asms'') asms' in @@ -410,4 +409,3 @@ primrec_cmd invs fctxt fixes params specs)); end; -