Stricter test: raise error if registration generates duplicate theorem.

--- a/src/FOL/ex/LocaleTest.thy	Wed Aug 19 19:35:46 2009 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Sat Sep 26 21:03:57 2009 +0200
@@ -390,6 +390,10 @@
 interpretation int2?: semi "op +"
   by unfold_locales  (* subsumed, thm int2.assoc not generated *)
 
+ML {* (PureThy.get_thms @{theory} "int2.assoc";
+    error "thm int2.assoc was generated")
+  handle ERROR "Unknown fact \"int2.assoc\"" => ([]:thm list); *}
+
 thm int.lone int.right.rone
   (* the latter comes through the sublocale relation *)