diff -r 53b20f786a5e -r 4efb68e5576d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Oct 08 18:13:09 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Mon Oct 08 18:13:10 2007 +0200
@@ -211,11 +211,7 @@
     val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
   in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
 
-fun add_def (name, prop) =
-  Theory.add_defs_i false false [(name, prop)] #>
-  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
-
-fun add_def_new (name, prop) thy =  (* FIXME inactive --- breaks codegen *)
+fun add_def (name, prop) thy =
   let
     val tfrees = rev (map TFree (Term.add_tfrees prop []));
     val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
@@ -224,8 +220,8 @@
 
     val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
     val thy' = Theory.add_defs_i false false [(name, prop')] thy;
-    val axm = Thm.get_axiom_i thy' (Sign.full_name thy' name);
-    val def = Thm.instantiate (recover_sorts, []) axm;
+    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
+    val def = Thm.instantiate (recover_sorts, []) axm';
   in (Drule.unvarify def, thy') end;
 
 in