src/HOL/SPARK/Tools/spark_vcs.ML

--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Aug 03 16:08:02 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Aug 04 17:40:48 2011 +0200
@@ -372,8 +372,11 @@
        end)
 
   | add_type_def prfx (s, Pending_Type) (ids, thy) =
-      (check_no_assoc thy prfx s;
-       (ids, Typedecl.typedecl_global (Binding.name s, [], NoSyn) thy |> snd));
+      (ids,
+       case get_type thy prfx s of
+         SOME _ => thy
+       | NONE => Typedecl.typedecl_global
+           (Binding.name s, [], NoSyn) thy |> snd);
 
 
 fun term_of_expr thy prfx types pfuns =