CookBook/Package/simple_inductive_package.ML
changeset 116 c9ff326e3ce5
parent 111 3798baeee55f
child 118 5f003fdf2653
--- a/CookBook/Package/simple_inductive_package.ML	Fri Feb 13 14:15:28 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sat Feb 14 00:11:50 2009 +0000
@@ -6,6 +6,7 @@
     (Binding.binding * typ) list ->  (*{parameters}*)
     ((Binding.binding * Attrib.src list) * term) list ->  (*{rules}*)
     local_theory -> local_theory
+
   val add_inductive:
     (Binding.binding * string option * mixfix) list ->  (*{predicates}*)
     (Binding.binding * string option * mixfix) list ->  (*{parameters}*)
@@ -170,7 +171,7 @@
 end;
 (* @end *)
 
-(* @chunk syntax *)
+(* @chunk parser *)
 val parser = 
    OuterParse.opt_target --
    OuterParse.fixes -- 
@@ -180,7 +181,9 @@
           OuterParse.!!! 
             (OuterParse.enum1 "|" 
                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+(* @end *)
 
+(* @chunk syntax *)
 val ind_decl =
   parser >>
     (fn (((loc, preds), params), specs) =>