src/FOL/ex/LocaleTest.thy
changeset 28235 89e4d2232ed2
parent 28085 914183e229e9
child 28611 983c1855a7af
--- a/src/FOL/ex/LocaleTest.thy	Tue Sep 16 12:25:26 2008 +0200
+++ b/src/FOL/ex/LocaleTest.thy	Tue Sep 16 12:26:15 2008 +0200
@@ -97,8 +97,10 @@
 
 locale IB = fixes b assumes asm_B [simp]: "b = b"
 
-locale IC = IA + IB + assumes asm_C: "c = c"
-  (* TODO: independent type var in c, prohibit locale declaration *)
+locale IC = IA + IB + assumes asm_C: "b = b"
+
+locale IC' = IA + IB + assumes asm_C: "c = c"
+  (* independent type var in c *)
 
 locale ID = IA + IB + fixes d defines def_D: "d == (a = b)"