| changeset 42806 | 4b660cdab9b7 |
| parent 42364 | 8c674b3b8e44 |
| child 43278 | 1fbdcebb364b |
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat May 14 16:22:53 2011 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat May 14 16:27:47 2011 +0200 @@ -34,7 +34,7 @@ gen_res_inst_tac_term (K Drule.cterm_instantiate) []; fun cut_inst_tac_term' tinst th = - res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th); + res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th); fun get_dyn_thm thy name atom_name = Global_Theory.get_thm thy name handle ERROR _ =>