--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 04 14:42:11 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Oct 04 14:42:47 2007 +0200
@@ -73,7 +73,7 @@
|> addsmps "psimps" [] psimps
||> fold_option (snd oo addsmps "simps" []) trsimps
||>> note_theorem ((qualify "pinduct",
- [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
+ [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts)
||>> note_theorem ((qualify "termination", []), [termination])
||> (snd o note_theorem ((qualify "cases", []), [cases]))
||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros