src/HOL/Nominal/nominal_fresh_fun.ML
changeset 27187 17b63e145986
parent 26343 0dd2eab7b296
child 27239 f2f42f9fa09d
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 22:41:03 2008 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jun 12 23:12:54 2008 +0200
     1.3 @@ -58,7 +58,7 @@
     1.4  
     1.5  fun get_dyn_thm thy name atom_name =
     1.6    PureThy.get_thm thy name handle ERROR _ =>
     1.7 -    raise ERROR ("The atom type "^atom_name^" is not defined.");
     1.8 +    error ("The atom type "^atom_name^" is not defined.");
     1.9  
    1.10  (* End of function waiting to be in the library :o) *)
    1.11