# HG changeset patch
# User haftmann
# Date 1366304222 -7200
# Node ID 88f7f38d5cb93c2523f177aa95642f94ae6d34cb
# Parent  4fd969609b4d92c1742d1f438866f37016044873
spelling

diff -r 4fd969609b4d -r 88f7f38d5cb9 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Thu Apr 18 18:55:23 2013 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Thu Apr 18 18:57:02 2013 +0200
@@ -142,7 +142,7 @@
       if not (Term.has_abs t)
       then if fold_aterms (fn Const _ => I | _ => K false) t true
         then SOME (HOLogic.reflect_term t)
-        else error "Cannot termify expression containing variables"
+        else error "Cannot termify expression containing variable"
       else error "Cannot termify expression containing abstraction"
   | subst_termify_app (t, ts) = case map_default subst_termify ts
      of SOME ts' => SOME (list_comb (t, ts'))