src/HOL/Nominal/nominal_inductive.ML
changeset 35232 f588e1169c8b
parent 33968 f94fb13ecbb3
child 36323 655e2d74de3a
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 11:56:11 2010 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Fri Feb 19 16:11:45 2010 +0100
     1.3 @@ -274,7 +274,7 @@
     1.4      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     1.5      val pt2_atoms = map (fn aT => PureThy.get_thm thy
     1.6        ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     1.7 -    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
     1.8 +    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss
     1.9        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    1.10        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    1.11          NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];
    1.12 @@ -455,7 +455,7 @@
    1.13                     concl))
    1.14            in map mk_prem prems end) cases_prems;
    1.15  
    1.16 -    val cases_eqvt_ss = Simplifier.theory_context thy HOL_ss
    1.17 +    val cases_eqvt_ss = Simplifier.global_context thy HOL_ss
    1.18        addsimps eqvt_thms @ swap_simps @ perm_pi_simp
    1.19        addsimprocs [NominalPermeq.perm_simproc_app,
    1.20          NominalPermeq.perm_simproc_fun];
    1.21 @@ -611,7 +611,7 @@
    1.22           atoms)
    1.23        end;
    1.24      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    1.25 -    val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps
    1.26 +    val eqvt_ss = Simplifier.global_context thy HOL_basic_ss addsimps
    1.27        (NominalThmDecls.get_eqvt_thms ctxt @ perm_pi_simp) addsimprocs
    1.28        [mk_perm_bool_simproc names,
    1.29         NominalPermeq.perm_simproc_app, NominalPermeq.perm_simproc_fun];