src/HOL/Tools/typedef_package.ML
changeset 27353 71c4dd53d4cb
parent 26939 1035c89b4c02
child 27691 ce171cbd4b93
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -260,7 +260,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val _ = OuterSyntax.keywords ["morphisms"];
     1.8 +val _ = OuterKeyword.keyword "morphisms";
     1.9  
    1.10  val typedef_decl =
    1.11    Scan.optional (P.$$$ "(" |--