Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
merged
authorberghofe
Thu, 04 Aug 2011 23:21:04 +0200
changeset 44031 b2158f199652
parent 44030 b63a6bc144cf (diff)
parent 44029 ce4e3090f01a (current diff)
child 44034 53a081c8873d
merged
--- 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 =
isabelle