changeset 35912 | b0e300bd3a2c |
parent 35906 | e0382e4b4da7 |
child 37108 | 00f13d3ad474 |
--- a/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 15:45:54 2010 -0700 +++ b/src/HOLCF/Tools/holcf_library.ML Mon Mar 22 15:53:25 2010 -0700 @@ -227,7 +227,7 @@ in (v::vs, mk_ssumT (T, U)) end - fun inj [] = error "mk_sinjects: empty list" + fun inj [] = raise Fail "mk_sinjects: empty list" | inj ((t, T)::[]) = ([t], T) | inj ((t, T)::ts) = combine (t, T) (inj ts); in