tuned;
authorwenzelm
Mon May 17 15:05:32 2010 +0200 (2010-05-17)
changeset 36958ad5313f1bd30
parent 36957 cdb9e83abfbe
child 36959 f5417836dbea
tuned;
src/HOL/Statespace/state_space.ML
src/HOL/Tools/inductive.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Mon May 17 15:02:44 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Mon May 17 15:05:32 2010 +0200
     1.3 @@ -32,10 +32,9 @@
     1.4         (string * typ) list -> theory -> theory
     1.5  
     1.6      val statespace_decl :
     1.7 -       OuterParse.token list ->
     1.8         ((string list * bstring) *
     1.9           ((string list * xstring * (bstring * bstring) list) list *
    1.10 -          (bstring * string) list)) * OuterParse.token list
    1.11 +          (bstring * string) list)) parser
    1.12  
    1.13  
    1.14      val neq_x_y : Proof.context -> term -> term -> thm option
     2.1 --- a/src/HOL/Tools/inductive.ML	Mon May 17 15:02:44 2010 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Mon May 17 15:05:32 2010 +0200
     2.3 @@ -83,8 +83,7 @@
     2.4      (binding * string option * mixfix) list ->
     2.5      (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     2.6      bool -> local_theory -> inductive_result * local_theory
     2.7 -  val gen_ind_decl: add_ind_def -> bool ->
     2.8 -    OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
     2.9 +  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
    2.10  end;
    2.11  
    2.12  structure Inductive: INDUCTIVE =