src/HOL/Tools/datatype_package.ML
changeset 17057 0934ac31985f
parent 16973 b2a894562b8f
child 17084 fb0a80aef0be
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:23 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue Aug 16 13:42:26 2005 +0200
     1.3 @@ -954,7 +954,7 @@
     1.4  
     1.5  (* outer syntax *)
     1.6  
     1.7 -local structure P = OuterParse and K = OuterSyntax.Keyword in
     1.8 +local structure P = OuterParse and K = OuterKeyword in
     1.9  
    1.10  val datatype_decl =
    1.11    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --