tuned outer syntax;

--- a/src/HOL/Tools/inductive_package.ML	Mon Aug 02 17:58:00 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Aug 02 17:58:23 1999 +0200
@@ -751,7 +751,7 @@
 fun ind_decl coind =
   (Scan.repeat1 P.term --| P.marg_comment) --
   (P.$$$ "intrs" |--
-    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment))) --
+    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment))) --
   Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
   Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1 --| P.marg_comment) []
   >> (Toplevel.theory o mk_ind coind);

--- a/src/HOL/Tools/primrec_package.ML	Mon Aug 02 17:58:00 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Mon Aug 02 17:58:23 1999 +0200
@@ -276,7 +276,7 @@
 
 val primrec_decl =
   Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
-    Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment);
+    Scan.repeat1 (P.opt_thm_name ":" -- P.prop --| P.marg_comment);
 
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl

--- a/src/HOL/Tools/typedef_package.ML	Mon Aug 02 17:58:00 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Mon Aug 02 17:58:23 1999 +0200
@@ -209,7 +209,7 @@
 
 val typedeclP =
   OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
-    (P.type_args -- P.name -- P.opt_mixfix --| P.marg_comment >> (fn ((vs, t), mx) =>
+    (P.type_args -- P.name -- P.opt_infix --| P.marg_comment >> (fn ((vs, t), mx) =>
       Toplevel.theory (add_typedecls [(t, vs, mx)])));