1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
     1.5  
     1.6  fun get_dyn_thm thy name atom_name =
     1.7 -  PureThy.get_thm thy name handle ERROR _ =>
     1.8 +  Global_Theory.get_thm thy name handle ERROR _ =>
     1.9      error ("The atom type "^atom_name^" is not defined.");
    1.10  
    1.11  (* End of function waiting to be in the library :o) *)
    1.12 @@ -126,8 +126,8 @@
    1.13      val thy = theory_of_thm thm;
    1.14      val ctxt = ProofContext.init_global thy;
    1.15      val ss = global_simpset_of thy;
    1.16 -    val abs_fresh = PureThy.get_thms thy "abs_fresh";
    1.17 -    val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
    1.18 +    val abs_fresh = Global_Theory.get_thms thy "abs_fresh";
    1.19 +    val fresh_perm_app = Global_Theory.get_thms thy "fresh_perm_app";
    1.20      val ss' = ss addsimps fresh_prod::abs_fresh;
    1.21      val ss'' = ss' addsimps fresh_perm_app;
    1.22      val x = hd (tl (OldTerm.term_vars (prop_of exI)));