--- a/src/HOL/ex/CodeEval.thy Wed Aug 30 08:29:30 2006 +0200
+++ b/src/HOL/ex/CodeEval.thy Wed Aug 30 08:30:09 2006 +0200
@@ -154,7 +154,6 @@
val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
-
fun conv ct =
let
val {thy, t, ...} = rep_cterm ct;
@@ -206,6 +205,6 @@
"rev [0, Suc 0, Suc 0] = [Suc 0, Suc 0, 0]" by eval
lemma
- "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc 0" by eval
+ "fst (snd (fst ( ((Some (2::nat), (Suc 0, ())), [0::nat]) ))) = Suc (Suc 0) - 1" by eval
end