1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Aug 03 16:08:02 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Aug 04 17:40:48 2011 +0200
     1.3 @@ -372,8 +372,11 @@
     1.4         end)
     1.5  
     1.6    | add_type_def prfx (s, Pending_Type) (ids, thy) =
     1.7 -      (check_no_assoc thy prfx s;
     1.8 -       (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
     1.9 +      (ids,
    1.10 +       case get_type thy prfx s of
    1.11 +         SOME _ => thy
    1.12 +       | NONE => Typedecl.typedecl_global
    1.13 +           (Binding.name s, [], NoSyn) thy |> snd);
    1.14  
    1.15  
    1.16  fun term_of_expr thy prfx types pfuns =