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