# HG changeset patch
# User ballarin
# Date 1253991837 -7200
# Node ID b52aa3bc736285a511efc905c151cf16c4fca992
# Parent  57fcca4e7c0eff946562813c352306928f8a4923
Stricter test: raise error if registration generates duplicate theorem.

diff -r 57fcca4e7c0e -r b52aa3bc7362 src/FOL/ex/LocaleTest.thy
--- 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 *)