1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:37:25 2011 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Dec 02 14:54:25 2011 +0100
     1.3 @@ -1003,8 +1003,8 @@
     1.4  
     1.5      val (((defs', vars''), ivars), (ids, thy')) =
     1.6        ((Symtab.empty |>
     1.7 -        Symtab.update ("false", (HOLogic.false_const, booleanN)) |>
     1.8 -        Symtab.update ("true", (HOLogic.true_const, booleanN)),
     1.9 +        Symtab.update ("false", (@{term False}, booleanN)) |>
    1.10 +        Symtab.update ("true", (@{term True}, booleanN)),
    1.11          Name.context),
    1.12         thy |> Sign.add_path (Long_Name.base_name ident)) |>
    1.13        fold (add_type_def prfx) (items types) |>