# HG changeset patch
# User wenzelm
# Date 1274101532 -7200
# Node ID ad5313f1bd30418e8458c27d75da3e3ce8d44af6
# Parent  cdb9e83abfbecd5c8201dd7eaf281ecf9dbc0160
tuned;

diff -r cdb9e83abfbe -r ad5313f1bd30 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Mon May 17 15:02:44 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Mon May 17 15:05:32 2010 +0200
@@ -32,10 +32,9 @@
        (string * typ) list -> theory -> theory
 
     val statespace_decl :
-       OuterParse.token list ->
        ((string list * bstring) *
          ((string list * xstring * (bstring * bstring) list) list *
-          (bstring * string) list)) * OuterParse.token list
+          (bstring * string) list)) parser
 
 
     val neq_x_y : Proof.context -> term -> term -> thm option
diff -r cdb9e83abfbe -r ad5313f1bd30 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Mon May 17 15:02:44 2010 +0200
+++ b/src/HOL/Tools/inductive.ML	Mon May 17 15:05:32 2010 +0200
@@ -83,8 +83,7 @@
     (binding * string option * mixfix) list ->
     (Attrib.binding * string) list -> (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
-  val gen_ind_decl: add_ind_def -> bool ->
-    OuterParse.token list -> (bool -> local_theory -> local_theory) * OuterParse.token list
+  val gen_ind_decl: add_ind_def -> bool -> (bool -> local_theory -> local_theory) parser
 end;
 
 structure Inductive: INDUCTIVE =