src/HOL/Nominal/nominal_fresh_fun.ML
changeset 42806 4b660cdab9b7
parent 42364 8c674b3b8e44
child 43278 1fbdcebb364b
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:22:53 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:27:47 2011 +0200
     1.3 @@ -34,7 +34,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 (RuleInsts.make_elim_preserve th);
     1.8 +  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
     1.9  
    1.10  fun get_dyn_thm thy name atom_name =
    1.11    Global_Theory.get_thm thy name handle ERROR _ =>