diff -r 9bfaf6819291 -r c7139609b67d src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 10:50:54 2011 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Tue Apr 19 14:57:09 2011 +0200
@@ -150,8 +150,8 @@
       | NONE => NONE)
   | subst_termify t = subst_termify_app (strip_comb t) 
 
-fun check_termify ts ctxt = map_default subst_termify ts
-  |> Option.map (rpair ctxt)
+fun check_termify ctxt ts =
+  the_default ts (map_default subst_termify ts);
 
 
 (** evaluation **)