1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 30 21:14:01 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Nov 30 23:30:08 2011 +0100
     1.3 @@ -305,7 +305,7 @@
     1.4                  val tyname = Sign.full_name thy tyb
     1.5                in
     1.6                  (thy |>
     1.7 -                 Datatype.add_datatype {strict = true, quiet = true} [s]
     1.8 +                 Datatype.add_datatype {strict = true, quiet = true}
     1.9                     [([], tyb, NoSyn,
    1.10                       map (fn s => (Binding.name s, [], NoSyn)) els)] |> snd |>
    1.11                   add_enum_type s tyname,