diff -r 87201c60ae7d -r 521cc9bf2958 src/HOL/ex/Sqrt_Script.thy
--- a/src/HOL/ex/Sqrt_Script.thy	Tue Sep 01 14:13:34 2009 +0200
+++ b/src/HOL/ex/Sqrt_Script.thy	Tue Sep 01 15:39:33 2009 +0200
@@ -6,7 +6,7 @@
 header {* Square roots of primes are irrational (script version) *}
 
 theory Sqrt_Script
-imports Complex_Main Primes
+imports Complex_Main "~~/src/HOL/Number_Theory/Primes"
 begin
 
 text {*
@@ -16,30 +16,30 @@
 
 subsection {* Preliminaries *}
 
-lemma prime_nonzero:  "prime p \<Longrightarrow> p \<noteq> 0"
-  by (force simp add: prime_def)
+lemma prime_nonzero:  "prime (p::nat) \<Longrightarrow> p \<noteq> 0"
+  by (force simp add: prime_nat_def)
 
 lemma prime_dvd_other_side:
-    "n * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
-  apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult)
+    "(n::nat) * n = p * (k * k) \<Longrightarrow> prime p \<Longrightarrow> p dvd n"
+  apply (subgoal_tac "p dvd n * n", blast dest: prime_dvd_mult_nat)
   apply auto
   done
 
-lemma reduction: "prime p \<Longrightarrow>
+lemma reduction: "prime (p::nat) \<Longrightarrow>
     0 < k \<Longrightarrow> k * k = p * (j * j) \<Longrightarrow> k < p * j \<and> 0 < j"
   apply (rule ccontr)
   apply (simp add: linorder_not_less)
   apply (erule disjE)
    apply (frule mult_le_mono, assumption)
    apply auto
-  apply (force simp add: prime_def)
+  apply (force simp add: prime_nat_def)
   done
 
 lemma rearrange: "(j::nat) * (p * j) = k * k \<Longrightarrow> k * k = p * (j * j)"
   by (simp add: mult_ac)
 
 lemma prime_not_square:
-    "prime p \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
+    "prime (p::nat) \<Longrightarrow> (\<And>k. 0 < k \<Longrightarrow> m * m \<noteq> p * (k * k))"
   apply (induct m rule: nat_less_induct)
   apply clarify
   apply (frule prime_dvd_other_side, assumption)
@@ -57,7 +57,7 @@
 *}
 
 theorem prime_sqrt_irrational:
-    "prime p \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
+    "prime (p::nat) \<Longrightarrow> x * x = real p \<Longrightarrow> 0 \<le> x \<Longrightarrow> x \<notin> \<rat>"
   apply (rule notI)
   apply (erule Rats_abs_nat_div_natE)
   apply (simp del: real_of_nat_mult
@@ -65,6 +65,6 @@
   done
 
 lemmas two_sqrt_irrational =
-  prime_sqrt_irrational [OF two_is_prime]
+  prime_sqrt_irrational [OF two_is_prime_nat]
 
 end