Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_package.ML
changeset 5179 819f90f278db
parent 5149 10f0be29c0d1
child 5303 22029546d109 
--- 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
isabelle