# HG changeset patch
# User berghofe
# Date 901277584 -7200
# Node ID 819f90f278db83daaf6c06ee7f72e3e69eee6005
# Parent  9337b230ff15648c061c9a2296257d733e2e625b
Replaced Nat.thy by NatDef.thy because Nat.thy depends on
inductive_package.

diff -r 9337b230ff15 -r 819f90f278db src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:50:34 1998 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jul 24 12:53:04 1998 +0200
@@ -288,7 +288,7 @@
 fun con_elim_tac simps =
   let val elim_tac = REPEAT o (eresolve_tac elim_rls)
   in ALLGOALS(EVERY'[elim_tac,
-                 asm_full_simp_tac (simpset_of Nat.thy addsimps simps),
+                 asm_full_simp_tac (simpset_of NatDef.thy addsimps simps),
                  elim_tac,
                  REPEAT o bound_hyp_subst_tac])
      THEN prune_params_tac