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