# HG changeset patch
# User haftmann
# Date 1242027638 -7200
# Node ID a95816259c77c96561719c7832d3afcfdd73ebf9
# Parent  e270f45ac0ec0875519f6c7fab67d60994a6719c
simplified unoverload/overload policy in code generator preprocessor

diff -r e270f45ac0ec -r a95816259c77 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Sun May 10 14:22:04 2009 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon May 11 09:40:38 2009 +0200
@@ -26,7 +26,7 @@
 fun add_thm NONE thm thy = Code.add_eqn thm thy
   | add_thm (SOME module_name) thm thy =
       case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm
-       of SOME (thm', _) => let val c = Code_Unit.const_eqn thm'
+       of SOME (thm', _) => let val c = Code_Unit.const_eqn thy thm'
             in thy
               |> ModuleData.map (Symtab.update (c, module_name))
               |> Code.add_eqn thm'
@@ -57,7 +57,6 @@
     val thms = Code.these_raw_eqns thy c'
       |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
       |> expand_eta thy
-      |> map (AxClass.overload thy)
       |> map_filter (meta_eq_to_obj_eq thy)
       |> Code_Unit.norm_varnames thy
       |> map (rpair opt_name)