# HG changeset patch
# User berghofe
# Date 1312492864 -7200
# Node ID b2158f1996521b6ed7d1dc1b69e668da7807b94b
# Parent  b63a6bc144cfadde339f205db24038ceb27ce03a# Parent  ce4e3090f01a9742010182508d3e6963be5bc6f1
merged

diff -r ce4e3090f01a -r b2158f199652 src/HOL/SPARK/Tools/spark_vcs.ML
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Aug 04 07:33:08 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Aug 04 23:21:04 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 =