1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML Thu May 10 22:51:44 2012 +0200
1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Fri May 11 13:41:30 2012 +0200
1.3 @@ -1066,7 +1066,7 @@
1.4 Symtab.update ("true", (@{term True}, booleanN)),
1.5 Name.context),
1.6 thy |> Sign.add_path
1.7 - (if prfx = "" then Long_Name.base_name ident else prfx)) |>
1.8 + ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
1.9 fold (add_type_def prfx) (items types) |>
1.10 fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
1.11 ids_thy |>