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