src/HOL/ex/CodeEval.thy

 val oracle = ("Eval", fn (thy, Eval t) =>
   Logic.mk_equals (t, eval_term' thy t));
 
 val oracle_name = NameSpace.pack [Context.theory_name (the_context ()), fst oracle];
 
-
 fun conv ct =
   let
     val {thy, t, ...} = rep_cterm ct;
     val t' = HOLogic.dest_Trueprop t;
     val thm' = Thm.invoke_oracle_i thy oracle_name (thy, Eval t');

 
 lemma
   "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