src/HOL/Nominal/nominal_inductive2.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59936 b8ffc3dc9e24
     1.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -147,7 +147,7 @@
     1.4    let val env = Pattern.first_order_match thy (p, Thm.prop_of th)
     1.5      (Vartab.empty, Vartab.empty)
     1.6    in Thm.instantiate ([],
     1.7 -    map (Envir.subst_term env #> Thm.cterm_of thy) vs ~~ cts) th
     1.8 +    map (Envir.subst_term env #> Thm.global_cterm_of thy) vs ~~ cts) th
     1.9    end;
    1.10  
    1.11  fun prove_strong_ind s alt_name avoids ctxt =
    1.12 @@ -230,7 +230,7 @@
    1.13      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    1.14  
    1.15      val inductive_forall_def' = Drule.instantiate'
    1.16 -      [SOME (Thm.ctyp_of thy fsT)] [] inductive_forall_def;
    1.17 +      [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
    1.18  
    1.19      fun lift_pred' t (Free (s, T)) ts =
    1.20        list_comb (Free (s, fsT --> T), t :: ts);
    1.21 @@ -319,7 +319,7 @@
    1.22          val fs_atom = Global_Theory.get_thm thy
    1.23            ("fs_" ^ Long_Name.base_name atom ^ "1");
    1.24          val avoid_th = Drule.instantiate'
    1.25 -          [SOME (Thm.ctyp_of thy (fastype_of p))] [SOME (Thm.cterm_of thy p)]
    1.26 +          [SOME (Thm.global_ctyp_of thy (fastype_of p))] [SOME (Thm.global_cterm_of thy p)]
    1.27            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
    1.28          val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result
    1.29            (fn ctxt' => EVERY
    1.30 @@ -399,12 +399,12 @@
    1.31                   val pis'' = fold_rev (concat_perm #> map) pis' pis;
    1.32                   val ihyp' = inst_params thy vs_ihypt ihyp
    1.33                     (map (fold_rev (NominalDatatype.mk_perm [])
    1.34 -                      (pis' @ pis) #> Thm.cterm_of thy) params' @ [Thm.cterm_of thy z]);
    1.35 +                      (pis' @ pis) #> Thm.global_cterm_of thy) params' @ [Thm.global_cterm_of thy z]);
    1.36                   fun mk_pi th =
    1.37                     Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
    1.38                         addsimprocs [NominalDatatype.perm_simproc])
    1.39                       (Simplifier.simplify (put_simpset eqvt_ss ctxt')
    1.40 -                       (fold_rev (mk_perm_bool o Thm.cterm_of thy)
    1.41 +                       (fold_rev (mk_perm_bool o Thm.global_cterm_of thy)
    1.42                           (pis' @ pis) th));
    1.43                   val gprems2 = map (fn (th, t) =>
    1.44                     if null (preds_of ps t) then mk_pi th