src/Pure/Syntax/syn_trans.ML
changeset 18678 dd0c569fa43d
parent 18478 29a5070b517c
child 18857 c4b4fbd74ffb
--- a/src/Pure/Syntax/syn_trans.ML	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sat Jan 14 17:14:06 2006 +0100
@@ -203,7 +203,7 @@
 
 fun the_struct structs i =
   if 1 <= i andalso i <= length structs then List.nth (structs, i - 1)
-  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
+  else raise error ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
       Lexicon.free (the_struct structs 1)
@@ -424,7 +424,7 @@
 
 fun the_struct' structs s =
   [(case Lexicon.read_nat s of
-    SOME i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
+    SOME i => Ast.Variable (the_struct structs i handle ERROR _ => raise Match)
   | NONE => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
 
 fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =