--- 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
--- 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'))