# HG changeset patch
# User wenzelm
# Date 1205615249 -3600
# Node ID 9d2c375e242b5a0541bcffc317bdf63ca816b3f3
# Parent  89b9f7c186314a1d321bc51f32d7ba73d27449e8
avoid unclear fact references;

diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -322,7 +322,7 @@
     apply (frule is_type_pTs [OF wf], assumption+)
     apply clarify
     apply (drule rule [OF wf], assumption+)
-    apply (rule refl)
+    apply (rule HOL.refl)
     apply assumption+
     done
 qed
diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/NumberTheory/EvenOdd.thy
--- a/src/HOL/NumberTheory/EvenOdd.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/NumberTheory/EvenOdd.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -249,7 +249,7 @@
 
 lemma neg_one_power_eq_mod_m: "[| 2 < m; [(-1::int)^j = (-1::int)^k] (mod m) |]
     ==> ((-1::int)^j = (-1::int)^k)"
-  using neg_one_power [of j] and insert neg_one_power [of k]
+  using neg_one_power [of j] and ListMem.insert neg_one_power [of k]
   by (auto simp add: one_not_neg_one_mod_m zcong_sym)
 
 end
diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/NumberTheory/Gauss.thy
--- a/src/HOL/NumberTheory/Gauss.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/NumberTheory/Gauss.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -51,7 +51,7 @@
   using p_g_2 by auto
 
 lemma int_nat: "int (nat ((p - 1) div 2)) = (p - 1) div 2"
-  using insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
+  using ListMem.insert p_g_2 by (auto simp add: pos_imp_zdiv_nonneg_iff)
 
 lemma p_minus_one_l: "(p - 1) div 2 < p"
 proof -
diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -443,7 +443,7 @@
 lemmas test_bit_2p = refl [THEN test_bit_2p', unfolded word_size]
 
 lemmas nth_w2p = test_bit_2p [unfolded of_int_number_of_eq
-  word_of_int [symmetric] of_int_power]
+  word_of_int [symmetric] Int.of_int_power]
 
 lemma uint_2p: 
   "(0::'a::len word) < 2 ^ n ==> uint (2 ^ n::'a::len word) = 2 ^ n"
diff -r 89b9f7c18631 -r 9d2c375e242b src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/HOL/Word/WordShift.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -1093,7 +1093,7 @@
 lemma word_rsplit_empty_iff_size:
   "(word_rsplit w = []) = (size w = 0)" 
   unfolding word_rsplit_def bin_rsplit_def word_size
-  by (simp add: bin_rsplit_aux_simp_alt Let_def split: split_split)
+  by (simp add: bin_rsplit_aux_simp_alt Let_def split: Product_Type.split_split)
 
 lemma test_bit_rsplit:
   "sw = word_rsplit w ==> m < size (hd sw :: 'a :: len word) ==> 
diff -r 89b9f7c18631 -r 9d2c375e242b src/ZF/UNITY/AllocImpl.thy
--- a/src/ZF/UNITY/AllocImpl.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -1,4 +1,4 @@
-(*Title: ZF/UNITY/AllocImpl
+(*  Title: ZF/UNITY/AllocImpl.thy
     ID:    $Id$
     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     Copyright   2002  University of Cambridge
@@ -124,7 +124,8 @@
 
 (** Safety property: (28) **)
 lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
-apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def
+  Increasing.increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
 apply (auto dest: ActsD)
 apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
 apply auto
diff -r 89b9f7c18631 -r 9d2c375e242b src/ZF/UNITY/ClientImpl.thy
--- a/src/ZF/UNITY/ClientImpl.thy	Sat Mar 15 22:07:28 2008 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy	Sat Mar 15 22:07:29 2008 +0100
@@ -121,7 +121,7 @@
 "client_prog: program guarantees Incr(lift(ask)) Int Incr(lift(rel))"
 apply (unfold guar_def)
 apply (auto intro!: increasing_imp_Increasing 
-            simp add: client_prog_ok_iff increasing_def preserves_imp_prefix)
+            simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
 apply (safety, force, force)+
 done