src/HOL/Nominal/nominal_fresh_fun.ML
changeset 27239 f2f42f9fa09d
parent 27187 17b63e145986
child 28397 389c5e494605
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Jun 16 17:56:08 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Mon Jun 16 22:13:39 2008 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4    gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
     1.5  
     1.6  fun cut_inst_tac_term' tinst th =
     1.7 -  res_inst_tac_term' tinst false (Tactic.make_elim_preserve th);
     1.8 +  res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
     1.9  
    1.10  fun get_dyn_thm thy name atom_name =
    1.11    PureThy.get_thm thy name handle ERROR _ =>