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 =