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
authorhaftmann
Fri, 05 Aug 2011 00:14:08 +0200
changeset 44034 53a081c8873d
parent 44031 b2158f199652 (diff)
parent 44033 bc45393f497b (current diff)
child 44035 322d1657c40c
merged
--- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Aug 04 20:11:39 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Fri Aug 05 00:14:08 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