# HG changeset patch
# User haftmann
# Date 1180120133 -7200
# Node ID 669d7391df1a1cf1a08d330b64089a3c416b9479
# Parent  7cb68a8708c11aec6476a3ab49193d8254d246b8
improved error handling

diff -r 7cb68a8708c1 -r 669d7391df1a src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Fri May 25 21:08:52 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Fri May 25 21:08:53 2007 +0200
@@ -566,7 +566,7 @@
         else CodegenFunc.bad_thm ("Type\n" ^ CodegenConsts.string_of_typ thy ty
            ^ "\nof defining equation\n"
            ^ string_of_thm thm
-           ^ "\nis incompatible declared function type\n"
+           ^ "\nis incompatible with declared function type\n"
            ^ CodegenConsts.string_of_typ thy ty_decl)
       end;
     fun check_typ (const as (c, _), thm) =
@@ -658,12 +658,12 @@
 
 fun add_inline thm thy =
   (map_exec_purge NONE o map_preproc o apfst o apfst)
-    (insert Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
+    (insert Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun del_inline thm thy =
   (map_exec_purge NONE o map_preproc o apfst o apfst)
-    (remove Thm.eq_thm_prop (CodegenFunc.mk_rew thm)) thy;
+    (remove Thm.eq_thm_prop (CodegenFunc.error_thm CodegenFunc.mk_rew thm)) thy;
         (*fully applied in order to get right context for mk_rew!*)
 
 fun add_inline_proc (name, f) =