# HG changeset patch
# User nipkow
# Date 1366309130 -7200
# Node ID 89f0d01371a8641208522efdb87a019f4a8e00b2
# Parent  88f7f38d5cb93c2523f177aa95642f94ae6d34cb# Parent  17b992f19b51b33924754da9693c21f4a98df3b4
merged

diff -r 17b992f19b51 -r 89f0d01371a8 src/Doc/Codegen/Evaluation.thy
--- a/src/Doc/Codegen/Evaluation.thy	Thu Apr 18 20:18:37 2013 +0200
+++ b/src/Doc/Codegen/Evaluation.thy	Thu Apr 18 20:18:50 2013 +0200
@@ -156,7 +156,7 @@
   @{text "SOME t'"} in the first case, @{text "NONE"} in the
   second, and propagating the exception in the third case.  A strict
   variant of plain evaluation either yields @{text "t'"} or propagates
-  any exception, a liberal variant caputures any exception in a result
+  any exception, a liberal variant captures any exception in a result
   of type @{text "Exn.result"}.
   
   For property conversion (which coincides with conversion except for
diff -r 17b992f19b51 -r 89f0d01371a8 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Thu Apr 18 20:18:37 2013 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Thu Apr 18 20:18:50 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'))