src/Pure/pure_thy.ML

   NameSelection of string * interval list |
   Fact of string;
 
 fun name_of_thmref (Name name) = name
   | name_of_thmref (NameSelection (name, _)) = name
-  | name_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
+  | name_of_thmref (Fact _) = error "Illegal literal fact";
 
 fun map_name_of_thmref f (Name name) = Name (f name)
   | map_name_of_thmref f (NameSelection (name, is)) = NameSelection (f name, is)
   | map_name_of_thmref _ thmref = thmref;
 
 fun string_of_thmref (Name name) = name
   | string_of_thmref (NameSelection (name, is)) =
       name ^ enclose "(" ")" (commas (map string_of_interval is))
-  | string_of_thmref (Fact _) = raise ERROR_MESSAGE "Illegal literal fact";
+  | string_of_thmref (Fact _) = error "Illegal literal fact";
 
 
 (* select_thm *)
 
 fun select_thm (Name _) thms = thms

 
 
 (* thms_containing etc. *)
 
 fun valid_thms thy (thmref, ths) =
-  (case try (transform_error (get_thms thy)) thmref of
+  (case try (get_thms thy) thmref of
     NONE => false
   | SOME ths' => Thm.eq_thms (ths, ths'));
 
 fun thms_containing theory spec =
   (theory :: Theory.ancestors_of theory)