CookBook/Package/simple_inductive_package.ML
changeset 120 c39f83d8daeb
parent 118 5f003fdf2653
child 121 26e5b41faa74
--- a/CookBook/Package/simple_inductive_package.ML	Sat Feb 14 16:09:04 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sun Feb 15 18:58:21 2009 +0000
@@ -155,16 +155,19 @@
   end
 (* @end *)
 
-(* @chunk add_inductive *)
+(* @chunk read_specification *)
 fun read_specification' vars specs lthy =
 let 
   val specs' = map (fn (a, s) => [(a, [s])]) specs
-  val ((varst, specst), _) = Specification.read_specification vars specs' lthy
+  val ((varst, specst), _) = 
+                   Specification.read_specification vars specs' lthy
   val specst' = map (apsnd the_single) specst
 in   
   (varst, specst')
 end 
+(* @end *)
 
+(* @chunk add_inductive *)
 fun add_inductive preds params specs lthy =
 let
   val (vars, specs') = read_specification' (preds @ params) specs lthy;
@@ -176,7 +179,7 @@
 (* @end *)
 
 (* @chunk parser *)
-val parser = 
+val spec_parser = 
    OuterParse.opt_target --
    OuterParse.fixes -- 
    OuterParse.for_fixes --
@@ -189,7 +192,7 @@
 
 (* @chunk syntax *)
 val ind_decl =
-  parser >>
+  spec_parser >>
     (fn (((loc, preds), params), specs) =>
       Toplevel.local_theory loc (add_inductive preds params specs))