src/HOL/Tools/function_package/fundef_package.ML
changeset 24830 a7b3ab44d993
parent 24722 59fd5cceccd7
child 24861 cc669ca5f382
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 04 14:42:11 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 04 14:42:47 2007 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4              |> addsmps "psimps" [] psimps
     1.5              ||> fold_option (snd oo addsmps "simps" []) trsimps
     1.6              ||>> note_theorem ((qualify "pinduct",
     1.7 -                                [Attrib.internal (K (InductAttrib.induct_set ""))]), simple_pinducts)
     1.8 +                                [Attrib.internal (K (Induct.induct_set ""))]), simple_pinducts)
     1.9              ||>> note_theorem ((qualify "termination", []), [termination])
    1.10              ||> (snd o note_theorem ((qualify "cases", []), [cases]))
    1.11              ||> fold_option (snd oo curry note_theorem (qualify "domintros", [])) domintros