formal comments (still dummy);

--- a/src/HOL/Tools/datatype_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -670,7 +670,7 @@
 
 val datatype_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
-    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
+    (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix --| P.marg_comment));
 
 fun mk_datatype args =
   let

--- a/src/HOL/Tools/inductive_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -710,10 +710,11 @@
   #1 o add_inductive true coind sets atts (map P.triple_swap intrs) monos con_defs;
 
 fun ind_decl coind =
-  Scan.repeat1 P.term --
-  (P.$$$ "intrs" |-- P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term))) --
-  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] --
-  Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) []
+  (Scan.repeat1 P.term --| P.marg_comment) --
+  (P.$$$ "intrs" |--
+    P.!!! (P.opt_attribs -- Scan.repeat1 (P.opt_thm_name ":" -- P.term --| 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);
 
 val inductiveP =

--- a/src/HOL/Tools/primrec_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/primrec_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -265,7 +265,7 @@
 
 val primrec_decl =
   Scan.optional (P.$$$ "(" |-- P.name --| P.$$$ ")") "" --
-    Scan.repeat1 (P.opt_thm_name ":" -- P.term);
+    Scan.repeat1 (P.opt_thm_name ":" -- P.term --| P.marg_comment);
 
 val primrecP =
   OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl

--- a/src/HOL/Tools/recdef_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -139,7 +139,7 @@
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
 val recdef_decl =
-  P.name -- P.term -- Scan.repeat1 P.term --
+  P.name -- P.term -- Scan.repeat1 (P.term --| P.marg_comment) --
   Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] --
   Scan.option (P.$$$ "(" |-- P.$$$ "simpset" |-- P.!!! (P.name --| P.$$$ ")"))
   >> (fn ((((f, R), eqs), congs), ss) => #1 o add_recdef_x f R eqs ss congs);

--- a/src/HOL/Tools/record_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/record_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -882,7 +882,7 @@
 
 val record_decl =
   P.type_args -- P.name -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+")
-    -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ)));
+    -- Scan.repeat1 (P.name -- (P.$$$ "::" |-- P.typ) --| P.marg_comment));
 
 val recordP =
   OuterSyntax.command "record" "define extensible record" K.thy_decl

--- a/src/HOL/Tools/typedef_package.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Tue May 25 20:24:10 1999 +0200
@@ -15,9 +15,9 @@
     term -> string list -> thm list -> tactic option -> theory -> theory
   val add_typedef_i_no_def: string -> bstring * string list * mixfix ->
     term -> string list -> thm list -> tactic option -> theory -> theory
-  val typedef_proof: string -> bstring * string list * mixfix -> string
+  val typedef_proof: (string * (bstring * string list * mixfix) * string) * Comment.text
     -> bool -> theory -> ProofHistory.T
-  val typedef_proof_i: string -> bstring * string list * mixfix -> term
+  val typedef_proof_i: (string * (bstring * string list * mixfix) * term) * Comment.text
     -> bool -> theory -> ProofHistory.T
 end;
 
@@ -189,13 +189,13 @@
 fun typedef_attribute cset do_typedef (thy, thm) =
   (check_nonempty cset thm; (thy |> do_typedef, thm));
 
-fun gen_typedef_proof prep_term name typ set int thy =
+fun gen_typedef_proof prep_term ((name, typ, set), comment) int thy =
   let
     val (cset, do_typedef) = prepare_typedef prep_term false name typ set thy;
     val goal = Thm.term_of (goal_nonempty cset);
   in
     thy
-    |> IsarThy.theorem_i "" [typedef_attribute cset do_typedef] (goal, []) int
+    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;
@@ -209,16 +209,16 @@
 
 val typedeclP =
   OuterSyntax.command "typedecl" "HOL type declaration" K.thy_decl
-    (P.type_args -- P.name -- P.opt_mixfix >> (fn ((vs, t), mx) =>
+    (P.type_args -- P.name -- P.opt_mixfix --| P.marg_comment >> (fn ((vs, t), mx) =>
       Toplevel.theory (add_typedecls [(t, vs, mx)])));
 
 
 val typedef_proof_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") --
-    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term);
+    (P.type_args -- P.name) -- P.opt_infix -- (P.$$$ "=" |-- P.term) -- P.marg_comment;
 
-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;
+fun mk_typedef_proof ((((opt_name, (vs, t)), mx), A), comment) =
+  typedef_proof ((if_none opt_name (Syntax.type_name t mx), (t, vs, mx), A), comment);
 
 val typedefP =
   OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)" K.thy_goal

--- a/src/Pure/axclass.ML	Tue May 25 20:23:30 1999 +0200
+++ b/src/Pure/axclass.ML	Tue May 25 20:24:10 1999 +0200
@@ -30,10 +30,12 @@
     -> tactic option -> thm
   val goal_subclass: theory -> xclass * xclass -> thm list
   val goal_arity: theory -> xstring * xsort list * xclass -> thm list
-  val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
-  val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
-  val instance_arity_proof: xstring * xsort list * xclass -> bool -> theory -> ProofHistory.T
-  val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
+  val instance_subclass_proof: (xclass * xclass) * Comment.text -> bool -> theory -> ProofHistory.T
+  val instance_subclass_proof_i: (class * class) * Comment.text -> bool -> theory -> ProofHistory.T
+  val instance_arity_proof: (xstring * xsort list * xclass) * Comment.text
+    -> bool -> theory -> ProofHistory.T
+  val instance_arity_proof_i: (string * sort list * class) * Comment.text
+    -> bool -> theory -> ProofHistory.T
   val setup: (theory -> theory) list
 end;
 
@@ -403,10 +405,10 @@
 
 fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
 
-fun inst_proof mk_prop add_thms sig_prop int thy =
+fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
-  |> IsarThy.theorem_i "" [inst_attribute add_thms]
-    (mk_prop (Theory.sign_of thy) sig_prop, []) int;
+  |> IsarThy.theorem_i (("", [inst_attribute add_thms],
+    (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
 
 val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
 val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;
@@ -430,13 +432,15 @@
 
 val axclassP =
   OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
-    (P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) [] -- Scan.repeat P.spec_name
+    (((P.name -- Scan.optional (P.$$$ "<" |-- P.!!! (P.list1 P.xname)) []) --| P.marg_comment)
+      -- Scan.repeat (P.spec_name --| P.marg_comment)
       >> (fn (cls, axs) => Toplevel.theory (#1 o add_axclass cls axs)));
 
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
-    ((P.xname -- (P.$$$ "<" |-- P.xname) >> instance_subclass_proof ||
-      P.xname -- (P.$$$ "::" |-- P.simple_arity) >> (instance_arity_proof o P.triple2))
+    ((P.xname -- (P.$$$ "<" |-- P.xname) -- P.marg_comment >> instance_subclass_proof ||
+      (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) -- P.marg_comment
+        >> instance_arity_proof)
       >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val _ = OuterSyntax.add_parsers [axclassP, instanceP];