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