diff -r 7feb35deb6f6 -r 5f13912245ff src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Wed Sep 23 13:42:53 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Wed Sep 23 14:00:12 2009 +0200
@@ -169,7 +169,7 @@
   end;
 
 fun dest_randomT (Type ("fun", [@{typ Random.seed},
-  Type ("*", [Type ("*", [T, @{typ "unit => Code_Eval.term"}]) ,@{typ Random.seed}])])) = T
+  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
   | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
 
 (* destruction of intro rules *)
@@ -707,7 +707,7 @@
 end;
 
 (* termify_code:
-val termT = Type ("Code_Eval.term", []);
+val termT = Type ("Code_Evaluation.term", []);
 fun termifyT T = HOLogic.mk_prodT (T, HOLogic.unitT --> termT)
 *)
 (*
@@ -1198,7 +1198,7 @@
       val t1' = mk_valtermify_term t1
       val t2' = mk_valtermify_term t2
     in
-      Const ("Code_Eval.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
+      Const ("Code_Evaluation.valapp", termifyT T --> termifyT T1 --> termifyT T2) $ t1' $ t2'
     end
   | mk_valtermify_term _ = error "Not a valid term for mk_valtermify_term"
 *)