153           (preds ~~ inducts)) #>> maps snd) 

   153           (preds ~~ inducts)) #>> maps snd) 

   154     |> snd

   154     |> snd

   155   end

   155   end

   156 (* @end *)

   156 (* @end *)

   157 

   157 

   159 fun read_specification' vars specs lthy =

   159 fun read_specification' vars specs lthy =

   160 let 

   160 let 

   161   val specs' = map (fn (a, s) => [(a, [s])]) specs

   161   val specs' = map (fn (a, s) => [(a, [s])]) specs

   163   val specst' = map (apsnd the_single) specst

   164   val specst' = map (apsnd the_single) specst

   164 in   

   165 in   

   165   (varst, specst')

   166   (varst, specst')

   166 end 

   167 end 

   168 fun add_inductive preds params specs lthy =

   171 fun add_inductive preds params specs lthy =

   169 let

   172 let

   170   val (vars, specs') = read_specification' (preds @ params) specs lthy;

   173   val (vars, specs') = read_specification' (preds @ params) specs lthy;

   171   val (preds', params') = chop (length preds) vars;

   174   val (preds', params') = chop (length preds) vars;

   172   val params'' = map fst params'

   175   val params'' = map fst params'

   174   add_inductive_i preds' params'' specs' lthy

   177   add_inductive_i preds' params'' specs' lthy

   175 end;

   178 end;

   176 (* @end *)

   179 (* @end *)

   177 

   180 

   178 (* @chunk parser *)

   181 (* @chunk parser *)

   180    OuterParse.opt_target --

   183    OuterParse.opt_target --

   181    OuterParse.fixes -- 

   184    OuterParse.fixes -- 

   182    OuterParse.for_fixes --

   185    OuterParse.for_fixes --

   183    Scan.optional 

   186    Scan.optional 

   184        (OuterParse.$$$ "where" |--

   187        (OuterParse.$$$ "where" |--

   187                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []

   190                (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []

   188 (* @end *)

   191 (* @end *)

   189 

   192 

   190 (* @chunk syntax *)

   193 (* @chunk syntax *)

   191 val ind_decl =

   194 val ind_decl =

   193     (fn (((loc, preds), params), specs) =>

   196     (fn (((loc, preds), params), specs) =>

   194       Toplevel.local_theory loc (add_inductive preds params specs))

   197       Toplevel.local_theory loc (add_inductive preds params specs))

   195 

   198 

   196 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"

   199 val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"

   197           OuterKeyword.thy_decl ind_decl

   200           OuterKeyword.thy_decl ind_decl