src/HOL/Statespace/state_space.ML
changeset 36958 ad5313f1bd30
parent 36692 54b64d4ad524
child 36960 01594f816e3a
     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