--- a/src/HOL/Integ/Bin.thy Mon Oct 06 19:15:02 1997 +0200
+++ b/src/HOL/Integ/Bin.thy Mon Oct 06 19:15:22 1997 +0200
@@ -155,8 +155,8 @@
fun int_tr (*"_Int"*) [t as Free (str, _)] =
(const "integ_of_bin" $
- (mk_bin str handle ERROR => raise_term "int_tr" [t]))
- | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
+ (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
+ | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
| int_tr' (*"integ_of"*) _ = raise Match;
--- a/src/HOL/ex/String.thy Mon Oct 06 19:15:02 1997 +0200
+++ b/src/HOL/ex/String.thy Mon Oct 06 19:15:22 1997 +0200
@@ -58,7 +58,7 @@
fun char_tr (*"_Char"*) [Free (c, _)] =
if size c = 1 then mk_char c
else error ("Bad character: " ^ quote c)
- | char_tr (*"_Char"*) ts = raise_term "char_tr" ts;
+ | char_tr (*"_Char"*) ts = raise TERM ("char_tr", ts);
fun char_tr' (*"Char"*) [t1, t2] =
const "_Char" $ free (ssquote (dest_nibs t1 t2))
@@ -77,7 +77,7 @@
fun string_tr (*"_String"*) [Free (txt, _)] =
mk_string (map mk_char (explode txt))
- | string_tr (*"_String"*) ts = raise_term "string_tr" ts;
+ | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
fun cons_tr' (*"op #"*) [c, cs] =
const "_String" $ free (ssquote (implode (dest_char c :: dest_string cs)))
--- a/src/ZF/ex/Bin.thy Mon Oct 06 19:15:02 1997 +0200
+++ b/src/ZF/ex/Bin.thy Mon Oct 06 19:15:22 1997 +0200
@@ -160,8 +160,8 @@
fun int_tr (*"_Int"*) [t as Free (str, _)] =
(const "integ_of_bin" $
- (mk_bin str handle ERROR => raise_term "int_tr" [t]))
- | int_tr (*"_Int"*) ts = raise_term "int_tr" ts;
+ (mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
+ | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
fun int_tr' (*"integ_of"*) [t] = const "_Int" $ free (dest_bin t)
| int_tr' (*"integ_of"*) _ = raise Match;