src/HOL/Nominal/nominal_inductive.ML
changeset 39557 fe5722fce758
parent 39159 0dec18004e75
child 41228 e1fce873b814
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -271,21 +271,21 @@
     1.4             (NominalDatatype.fresh_const U T $ u $ t)) bvars)
     1.5               (ts ~~ binder_types (fastype_of p)))) prems;
     1.6  
     1.7 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     1.8 -    val pt2_atoms = map (fn aT => PureThy.get_thm thy
     1.9 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
    1.10 +    val pt2_atoms = map (fn aT => Global_Theory.get_thm thy
    1.11        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    1.12      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
    1.13        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.14        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    1.15          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.16 -    val fresh_bij = PureThy.get_thms thy "fresh_bij";
    1.17 -    val perm_bij = PureThy.get_thms thy "perm_bij";
    1.18 -    val fs_atoms = map (fn aT => PureThy.get_thm thy
    1.19 +    val fresh_bij = Global_Theory.get_thms thy "fresh_bij";
    1.20 +    val perm_bij = Global_Theory.get_thms thy "perm_bij";
    1.21 +    val fs_atoms = map (fn aT => Global_Theory.get_thm thy
    1.22        ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    1.23 -    val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
    1.24 -    val fresh_atm = PureThy.get_thms thy "fresh_atm";
    1.25 -    val swap_simps = PureThy.get_thms thy "swap_simps";
    1.26 -    val perm_fresh_fresh = PureThy.get_thms thy "perm_fresh_fresh";
    1.27 +    val exists_fresh' = Global_Theory.get_thms thy "exists_fresh'";
    1.28 +    val fresh_atm = Global_Theory.get_thms thy "fresh_atm";
    1.29 +    val swap_simps = Global_Theory.get_thms thy "swap_simps";
    1.30 +    val perm_fresh_fresh = Global_Theory.get_thms thy "perm_fresh_fresh";
    1.31  
    1.32      fun obtain_fresh_name ts T (freshs1, freshs2, ctxt) =
    1.33        let
    1.34 @@ -610,7 +610,7 @@
    1.35             | xs => error ("No such atoms: " ^ commas xs);
    1.36           atoms)
    1.37        end;
    1.38 -    val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.39 +    val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp";
    1.40      val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
    1.41        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    1.42        [mk_perm_bool_simproc names,