--- a/CookBook/Package/simple_inductive_package.ML	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML	Sat Feb 07 12:05:02 2009 +0000
@@ -9,14 +9,22 @@
   val add_inductive:
     (Binding.binding * string option * mixfix) list ->  (*{predicates}*)
     (Binding.binding * string option * mixfix) list ->  (*{parameters}*)
-    (Attrib.binding * string) list ->  (*{rules}*)
-    local_theory -> (thm list * thm list) * local_theory
+    (Attrib.binding * string list) list list ->  (*{rules}*)
+    local_theory -> local_theory
 end;
 (* @end *)
 
 structure SimpleInductivePackage: SIMPLE_INDUCTIVE_PACKAGE =
 struct
 
+fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P 
+
+fun inst_spec ct = Drule.instantiate'
+      [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec};
+
+val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
+val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp});
+
 fun add_inductive_i preds_syn params intrs lthy =
   let
     val params' = map (fn (p, T) => Free (Binding.base_name p, T)) params;
@@ -29,8 +37,6 @@
     val intrs' = map
       (ObjectLogic.atomize_term (ProofContext.theory_of lthy) o snd) intrs;
 
-    fun mk_all x P = HOLogic.all_const (fastype_of x) $ lambda x P;
-
     val (defs, lthy1) = fold_map (fn ((((R, _), syn), pred), Ts) =>
       let val zs = map Free (Variable.variant_frees lthy intrs'
         (map (pair "z") Ts))
@@ -53,9 +59,6 @@
     val cPs = map (cterm_of (ProofContext.theory_of lthy3)) Ps;
     val intrs'' = map (subst_free (preds ~~ Ps) o snd) intrs;
 
-    fun inst_spec ct = Drule.instantiate'
-      [SOME (ctyp_of_term ct)] [NONE, SOME ct] spec;
-
     fun prove_indrule ((R, P), Ts) =
       let
         val (znames, lthy4) =
@@ -80,9 +83,6 @@
 
     (* proving the introduction rules *)
     (* @chunk intro_rules *) 
-    val all_elims = fold (fn ct => fn th => th RS inst_spec ct);
-    val imp_elims = fold (fn th => fn th' => [th', th] MRS mp);
-
     fun prove_intr (i, (_, r)) =
       Goal.prove lthy2 [] [] r
         (fn {prems, context = ctxt} => EVERY
@@ -136,36 +136,39 @@
   end;
    
 (* @chunk add_inductive *)
-fun add_inductive preds_syn params_syn intro_srcs lthy =
-  let
-    val ((vars, specs), _) = Specification.read_specification
-      (preds_syn @ params_syn) (map (fn (a, s) => [(a, [s])]) intro_srcs)
-      lthy;
-    val (preds_syn', params_syn') = chop (length preds_syn) vars;
-    val intrs = map (apsnd the_single) specs
-  in
-    add_inductive_i preds_syn' (map fst params_syn') intrs lthy
-  end;
+fun add_inductive preds params specs lthy =
+ let
+    val ((vars, specs'), _) = Specification.read_specification (preds @ params) specs lthy;
+    val (preds', params') = chop (length preds) vars;
+    val specs'' = map (apsnd the_single) specs'
+    val params'' = map fst params'
+ in
+    snd (add_inductive_i preds' params'' specs'' lthy) 
+ end;
 (* @end *)
 
 
 (* outer syntax *)
+(* @chunk syntax *)
+val parser = 
+   OuterParse.opt_target --
+   OuterParse.fixes -- 
+   OuterParse.for_fixes --
+   Scan.optional 
+       (OuterParse.$$$ "where" |--
+          OuterParse.!!! 
+            (OuterParse.enum1 "|" 
+               ((SpecParse.opt_thm_name ":" -- 
+                   (OuterParse.prop >> single)) >> single))) []
 
-(* @chunk syntax *)
-local structure P = OuterParse and K = OuterKeyword in
 
 val ind_decl =
-  P.opt_target --
-  P.fixes -- P.for_fixes --
-  Scan.optional (P.$$$ "where" |--
-    P.!!! (P.enum1 "|" (SpecParse.opt_thm_name ":" -- P.prop))) [] >>
-  (fn (((loc, preds), params), specs) =>
-    Toplevel.local_theory loc (add_inductive preds params specs #> snd));
+    parser >>
+    (fn (((loc, preds), params), specs) =>
+      Toplevel.local_theory loc (add_inductive preds params specs));
 
 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
-  K.thy_decl ind_decl;
-
-end;
+  OuterKeyword.thy_decl ind_decl;
 (* @end *)
 
 end;