# HG changeset patch
# User krauss
# Date 1291366990 -3600
# Node ID ace26e2cee91f9e8c0e7534ca8daddcf5003b462
# Parent  e71d62a8fe5e51047a723b7c399b129136291afe
eliminated unqualified accesses of datatype facts -- it seems like they all of them were unintended

diff -r e71d62a8fe5e -r ace26e2cee91 src/HOL/MicroJava/BV/BVSpecTypeSafe.thy
--- a/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Dec 03 09:58:32 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVSpecTypeSafe.thy	Fri Dec 03 10:03:10 2010 +0100
@@ -231,7 +231,7 @@
       with wf less loc
       have "approx_stk G hp [xcp] ST'"
         by (auto simp add: sup_state_conv approx_stk_def approx_val_def 
-                 elim: conf_widen split: Err.split)
+                 elim: conf_widen split: err.split)
       moreover
       note len pc
       ultimately
@@ -702,7 +702,7 @@
   G,phi \<turnstile>JVM (None, hp, (stk,loc,C,sig,pc)#frs)\<surd>;
   fst (exec_instr (ins!pc) G hp stk loc C sig pc frs) = None \<rbrakk> 
 \<Longrightarrow> G,phi \<turnstile>JVM state'\<surd>"
-apply (clarsimp simp add: defs2 split_beta split: option.split List.split split_if_asm)
+apply (clarsimp simp add: defs2 split_beta split: option.split list.split split_if_asm)
 apply (frule conf_widen)
 prefer 2
   apply assumption
diff -r e71d62a8fe5e -r ace26e2cee91 src/HOL/Quotient_Examples/Quotient_Int.thy
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Dec 03 09:58:32 2010 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy	Fri Dec 03 10:03:10 2010 +0100
@@ -275,7 +275,7 @@
 proof (cases x, clarify)
   fix a b
   show "P (a, b)"
-  proof (induct a arbitrary: b rule: Nat.induct)
+  proof (induct a arbitrary: b rule: nat.induct)
     case zero
     show "P (0, b)" using assms by (induct b) auto
   next
diff -r e71d62a8fe5e -r ace26e2cee91 src/HOL/ex/set.thy
--- a/src/HOL/ex/set.thy	Fri Dec 03 09:58:32 2010 +0100
+++ b/src/HOL/ex/set.thy	Fri Dec 03 10:03:10 2010 +0100
@@ -205,7 +205,7 @@
 lemma "(\<forall>A. 0 \<in> A \<and> (\<forall>x \<in> A. Suc x \<in> A) \<longrightarrow> n \<in> A) \<and>
   P 0 \<and> (\<forall>x. P x \<longrightarrow> P (Suc x)) \<longrightarrow> P n"
   -- {* Example 11: needs a hint. *}
-by(metis Nat.induct)
+by(metis nat.induct)
 
 lemma
   "(\<forall>A. (0, 0) \<in> A \<and> (\<forall>x y. (x, y) \<in> A \<longrightarrow> (Suc x, Suc y) \<in> A) \<longrightarrow> (n, m) \<in> A)