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.
src/Pure/term_ord.ML
changeset 37852 a902f158b4fc
parent 35408 b48ab741683b
child 43794 49cbbe2768a8 
--- a/src/Pure/term_ord.ML	Tue Jul 20 14:41:13 2010 +0200
+++ b/src/Pure/term_ord.ML	Tue Jul 20 14:44:33 2010 +0200
@@ -84,7 +84,7 @@
   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
-  | atoms_ord _ = sys_error "atoms_ord";
+  | atoms_ord _ = raise Fail "atoms_ord";
 
 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
@@ -94,7 +94,7 @@
   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   | types_ord (Bound _, Bound _) = EQUAL
-  | types_ord _ = sys_error "types_ord";
+  | types_ord _ = raise Fail "types_ord";
 
 in
isabelle