--- 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;