Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TFL/tfl.ML
changeset 18678 dd0c569fa43d
parent 18358 0a733e11021a
child 18972 2905d1805e1e 
--- a/TFL/tfl.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/TFL/tfl.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -578,7 +578,7 @@
      val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon
                        theory Hilbert_Choice*)
          thm "Hilbert_Choice.tfl_some"
-         handle ERROR => error
+         handle ERROR msg => cat_error msg
     "defer_recdef requires theory Main or at least Hilbert_Choice as parent"
      val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th
  in {theory = theory, R=R1, SV=SV,
isabelle