src/HOL/Tools/inductive_package.ML
changeset 5179 819f90f278db
parent 5149 10f0be29c0d1
child 5303 22029546d109
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:50:34 1998 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:53:04 1998 +0200
     1.3 @@ -288,7 +288,7 @@
     1.4  fun con_elim_tac simps =
     1.5    let val elim_tac = REPEAT o (eresolve_tac elim_rls)
     1.6    in ALLGOALS(EVERY'[elim_tac,
     1.7 -                 asm_full_simp_tac (simpset_of Nat.thy addsimps simps),
     1.8 +                 asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
     1.9                   elim_tac,
    1.10                   REPEAT o bound_hyp_subst_tac])
    1.11       THEN prune_params_tac