diff -r 52d332f8f909 -r 5c8fb4fd67e0 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Tue May 19 13:57:31 2009 +0200
+++ b/src/HOL/RealDef.thy	Tue May 19 13:57:32 2009 +0200
@@ -1126,6 +1126,26 @@
 lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"
   by (simp add: of_rat_divide)
 
+definition (in term_syntax)
+  valterm_ratreal :: "rat \<times> (unit \<Rightarrow> Code_Eval.term) \<Rightarrow> real \<times> (unit \<Rightarrow> Code_Eval.term)" where
+  [code inline]: "valterm_ratreal k = Code_Eval.valtermify Ratreal {\<cdot>} k"
+
+notation fcomp (infixl "o>" 60)
+notation scomp (infixl "o\<rightarrow>" 60)
+
+instantiation real :: random
+begin
+
+definition
+  "random i = random i o\<rightarrow> (\<lambda>r. Pair (valterm_ratreal r))"
+
+instance ..
+
+end
+
+no_notation fcomp (infixl "o>" 60)
+no_notation scomp (infixl "o\<rightarrow>" 60)
+
 text {* Setup for SML code generator *}
 
 types_code