# HG changeset patch
# User berghofe
# Date 1312472448 -7200
# Node ID b63a6bc144cfadde339f205db24038ceb27ce03a
# Parent  3e5f8cc666dbd0cadc48d0759949f27bf82c2354
Pending FDL types may now be associated with Isabelle types as well.

diff -r 3e5f8cc666db -r b63a6bc144cf 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 =