src/HOL/Nominal/nominal_fresh_fun.ML
changeset 26343 0dd2eab7b296
parent 26337 44473c957672
child 27187 17b63e145986
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Wed Mar 19 22:50:42 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 20 00:20:44 2008 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4    res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
     1.5  
     1.6  fun get_dyn_thm thy name atom_name =
     1.7 -  dynamic_thm thy name handle ERROR _ =>
     1.8 +  PureThy.get_thm thy name handle ERROR _ =>
     1.9      raise 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 @@ -146,8 +146,8 @@
    1.13      val thy = theory_of_thm thm;
    1.14      val ctx = Context.init_proof thy;
    1.15      val ss = simpset_of thy;
    1.16 -    val abs_fresh = dynamic_thms thy "abs_fresh";
    1.17 -    val fresh_perm_app = dynamic_thms thy "fresh_perm_app";
    1.18 +    val abs_fresh = PureThy.get_thms thy "abs_fresh";
    1.19 +    val fresh_perm_app = PureThy.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 (term_vars (prop_of exI)));