src/HOL/Nominal/nominal_inductive.ML
changeset 59621 291934bac95e
parent 59586 ddf6deaadfe8
child 59936 b8ffc3dc9e24
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -204,7 +204,7 @@
     1.4      val fsT = TFree (fs_ctxt_tyname, ind_sort);
     1.5  
     1.6      val inductive_forall_def' = Drule.instantiate'
     1.7 -      [SOME (Thm.ctyp_of thy fsT)] [] inductive_forall_def;
     1.8 +      [SOME (Thm.global_ctyp_of thy fsT)] [] inductive_forall_def;
     1.9  
    1.10      fun lift_pred' t (Free (s, T)) ts =
    1.11        list_comb (Free (s, fsT --> T), t :: ts);
    1.12 @@ -338,7 +338,7 @@
    1.13                   val pis'' = fold (concat_perm #> map) pis' pis;
    1.14                   val env = Pattern.first_order_match thy (ihypt, Thm.prop_of ihyp)
    1.15                     (Vartab.empty, Vartab.empty);
    1.16 -                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.cterm_of thy))
    1.17 +                 val ihyp' = Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
    1.18                     (map (Envir.subst_term env) vs ~~
    1.19                      map (fold_rev (NominalDatatype.mk_perm [])
    1.20                        (rev pis' @ pis)) params' @ [z])) ihyp;
    1.21 @@ -346,7 +346,7 @@
    1.22                     Simplifier.simplify (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]
    1.23                         addsimprocs [NominalDatatype.perm_simproc])
    1.24                       (Simplifier.simplify (put_simpset eqvt_ss ctxt')
    1.25 -                       (fold_rev (mk_perm_bool o Thm.cterm_of thy)
    1.26 +                       (fold_rev (mk_perm_bool o Thm.global_cterm_of thy)
    1.27                           (rev pis' @ pis) th));
    1.28                   val (gprems1, gprems2) = split_list
    1.29                     (map (fn (th, t) =>
    1.30 @@ -505,8 +505,8 @@
    1.31                    val freshs2' = NominalDatatype.mk_not_sym freshs2;
    1.32                    val pis = map (NominalDatatype.perm_of_pair)
    1.33                      ((freshs1 ~~ map fst qs) @ (params' ~~ freshs1));
    1.34 -                  val mk_pis = fold_rev mk_perm_bool (map (Thm.cterm_of thy) pis);
    1.35 -                  val obj = Thm.cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
    1.36 +                  val mk_pis = fold_rev mk_perm_bool (map (Thm.global_cterm_of thy) pis);
    1.37 +                  val obj = Thm.global_cterm_of thy (foldr1 HOLogic.mk_conj (map (map_aterms
    1.38                       (fn x as Free _ =>
    1.39                             if member (op =) args x then x
    1.40                             else (case AList.lookup op = tab x of
    1.41 @@ -630,9 +630,9 @@
    1.42              val prems' = map (fn th => the_default th (map_thm ctxt''
    1.43                (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems;
    1.44              val prems'' = map (fn th => Simplifier.simplify eqvt_simpset
    1.45 -              (mk_perm_bool (Thm.cterm_of thy pi) th)) prems';
    1.46 -            val intr' = Drule.cterm_instantiate (map (Thm.cterm_of thy) vs ~~
    1.47 -               map (Thm.cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
    1.48 +              (mk_perm_bool (Thm.global_cterm_of thy pi) th)) prems';
    1.49 +            val intr' = Drule.cterm_instantiate (map (Thm.global_cterm_of thy) vs ~~
    1.50 +               map (Thm.global_cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params)
    1.51                 intr
    1.52            in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
    1.53            end) ctxt' 1 st