# HG changeset patch
# User haftmann
# Date 1236928578 -3600
# Node ID 072daf3914c05d9a73cc621160259fca7906d8c3
# Parent  1a1a9ca977d6aedd8b6129ffb8f94fb4bfd6ed84
dropped spurious `quote` tags

diff -r 1a1a9ca977d6 -r 072daf3914c0 src/HOL/Library/Random.thy
--- a/src/HOL/Library/Random.thy	Thu Mar 12 23:01:25 2009 +0100
+++ b/src/HOL/Library/Random.thy	Fri Mar 13 08:16:18 2009 +0100
@@ -58,10 +58,10 @@
 
 subsection {* Base selectors *}
 
-fun %quote iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
+fun iterate :: "index \<Rightarrow> ('b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a" where
   "iterate k f x = (if k = 0 then Pair x else f x o\<rightarrow> iterate (k - 1) f)"
 
-definition %quote range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
+definition range :: "index \<Rightarrow> seed \<Rightarrow> index \<times> seed" where
   "range k = iterate (log 2147483561 k)
       (\<lambda>l. next o\<rightarrow> (\<lambda>v. Pair (v + l * 2147483561))) 1
     o\<rightarrow> (\<lambda>v. Pair (v mod k))"