1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Jul 23 09:28:03 2012 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Jul 23 18:52:10 2012 +0200
     1.3 @@ -1067,8 +1067,13 @@
     1.4         | NONE => error ("Bad definitions: " ^ rulenames defs));
     1.5  
     1.6  fun set_vcs ({types, vars, consts, funs} : decls)
     1.7 -      (rules, _) ((_, ident), vcs) path prfx thy =
     1.8 +      (rules, _) ((_, ident), vcs) path opt_prfx thy =
     1.9    let
    1.10 +    val prfx' =
    1.11 +      if opt_prfx = "" then
    1.12 +        space_implode "__" (Long_Name.explode (Long_Name.qualifier ident))
    1.13 +      else opt_prfx;
    1.14 +    val prfx = to_lower prfx';
    1.15      val {pfuns, ...} = VCs.get thy;
    1.16      val (defs, rules') = partition_opt dest_def rules;
    1.17      val consts' =
    1.18 @@ -1094,7 +1099,7 @@
    1.19          Symtab.update ("true", (@{term True}, booleanN)),
    1.20          Name.context),
    1.21         thy |> Sign.add_path
    1.22 -         ((if prfx = "" then "" else prfx ^ "__") ^ Long_Name.base_name ident)) |>
    1.23 +         ((if prfx' = "" then "" else prfx' ^ "__") ^ Long_Name.base_name ident)) |>
    1.24        fold (add_type_def prfx) (items types) |>
    1.25        fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
    1.26          ids_thy |>