| changeset 22101 | 6d13239d5f52 |
| parent 20342 | 4392003fcbfa |
| child 24707 | dfeb98f84e93 |
--- a/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -205,7 +205,7 @@ local structure P = OuterParse and K = OuterKeyword in -val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop); +val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl