Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
spelling
authorhaftmann
Thu, 18 Apr 2013 18:57:02 +0200
changeset 51714 88f7f38d5cb9
parent 51713 4fd969609b4d
child 51716 89f0d01371a8
spelling
src/HOL/Tools/code_evaluation.ML file | annotate | diff | comparison | revisions 
--- 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'))
isabelle