diff -r 8bcc8809ed3b -r abfdccaed085 src/HOL/ex/Classical.thy
--- a/src/HOL/ex/Classical.thy	Thu Apr 19 16:38:59 2007 +0200
+++ b/src/HOL/ex/Classical.thy	Thu Apr 19 18:23:11 2007 +0200
@@ -849,19 +849,19 @@
     by (meson equalityI 2) 
   have 11: "!!U V. U \<notin> S | V \<notin> S | V = U"
     by (meson 10 2) 
-  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
+  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
     by (meson subsetI 11)
-  have 14: "!!U V. S \<subseteq> U | S \<subseteq> V | Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S V"
+  have 14: "!!U V. S \<subseteq> U | S \<subseteq> V | sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S V"
     by (meson subsetI 13)
-  have 29: "!!U V. S \<subseteq> U |  Set_XsubsetI_sko1_ S U = Set_XsubsetI_sko1_ S {V}"
+  have 29: "!!U V. S \<subseteq> U |  sko_Set_XsubsetI_1_ S U = sko_Set_XsubsetI_1_ S {V}"
     by (meson 1 14)
-  have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
     by (meson 1 29)
     (*hacked here while we wait for Metis: !!U V complicates proofs.*)
-  have 82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+  have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
     apply (insert 58 [of U V], erule ssubst)
     by (meson 58 subsetI)
-  have 85: "Set_XsubsetI_sko1_ S {U} \<notin> {V}"
+  have 85: "sko_Set_XsubsetI_1_ S {U} \<notin> {V}"
     by (meson 1 82)
   show False
     by (meson insertI1 85)
@@ -874,12 +874,12 @@
   fix S :: "'a set set"
   assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
      and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
-  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = Set_XsubsetI_sko1_ S V"
+  have 13: "!!U V. U \<notin> S | S \<subseteq> V | U = sko_Set_XsubsetI_1_ S V"
     by (meson subsetI equalityI 2)
-  have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
     by (meson 1 subsetI 13)
     (*hacked here while we wait for Metis: !!U V complicates proofs.*)
-  have 82: "Set_XsubsetI_sko1_ S {U} \<notin> {V} | S \<subseteq> {V}"
+  have 82: "sko_Set_XsubsetI_1_ S {U} \<notin> {V} | S \<subseteq> {V}"
     apply (insert 58 [of U V], erule ssubst)
     by (meson 58 subsetI)
   show False
@@ -893,7 +893,7 @@
   fix S :: "'a set set"
   assume 1: "\<And>Z. ~ (S \<subseteq> {Z})"
      and 2: "\<And>X Y. X \<notin> S | Y \<notin> S | X \<subseteq> Y"
-  have 58: "!!U V. Set_XsubsetI_sko1_ S {U} = Set_XsubsetI_sko1_ S {V}"
+  have 58: "!!U V. sko_Set_XsubsetI_1_ S {U} = sko_Set_XsubsetI_1_ S {V}"
     by (meson 1 subsetI_0 equalityI 2)
   show False
     by (iprover intro: subsetI_1 insertI1 1 58 elim: ssubst)