--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Sep 17 16:38:11 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Fri Sep 17 17:31:20 2010 +0200
@@ -791,7 +791,7 @@
"k < l \<Longrightarrow> divmod_rel k l 0 k"
| "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
-code_pred divmod_rel ..
+code_pred divmod_rel .
thm divmod_rel.equation
value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"