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