src/HOL/Nominal/nominal_fresh_fun.ML
changeset 32149 ef59550a55d3
parent 30549 d2d7874648bd
child 33034 66ef64a5f122
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -143,7 +143,7 @@
     1.4    let
     1.5      val thy = theory_of_thm thm;
     1.6      val ctx = Context.init_proof thy;
     1.7 -    val ss = simpset_of thy;
     1.8 +    val ss = global_simpset_of thy;
     1.9      val abs_fresh = PureThy.get_thms thy "abs_fresh";
    1.10      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
    1.11      val ss' = ss addsimps fresh_prod::abs_fresh;