src/HOL/Tools/typedef_package.ML
changeset 6723 f342449d73ca
parent 6690 acbcf8085166
child 6729 b6e167580a32
--- a/src/HOL/Tools/typedef_package.ML	Mon May 24 21:56:14 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Mon May 24 21:57:13 1999 +0200
@@ -205,24 +205,26 @@
 
 (** outer syntax **)
 
-local open OuterParse in
+local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val typedeclP =
-  OuterSyntax.command "typedecl" "HOL type declaration"
-    (type_args -- name -- opt_mixfix >> (fn ((vs, t), mx) =>
+  OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
+    (P.type_args -- P.name -- P.opt_mixfix >> (fn ((vs, t), mx) =>
       Toplevel.theory (add_typedecls [(t, vs, mx)])));
 
+
 val typedef_proof_decl =
-  Scan.option ($$$ "(" |-- name --| $$$ ")") --
-    (type_args -- name) -- opt_infix -- ($$$ "=" |-- term);
+  Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
+    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term);
 
 fun mk_typedef_proof (((opt_name, (vs, t)), mx), A) =
   typedef_proof (if_none opt_name (Syntax.type_name t mx)) (t, vs, mx) A;
 
 val typedefP =
-  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
+  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal
     (typedef_proof_decl >> (Toplevel.print oo (Toplevel.theory_to_proof o mk_typedef_proof)));
 
+
 val _ = OuterSyntax.add_parsers [typedeclP, typedefP];
 
 end;