1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Oct 08 18:13:09 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Oct 08 18:13:10 2007 +0200
     1.3 @@ -211,11 +211,7 @@
     1.4      val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
     1.5    in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
     1.6  
     1.7 -fun add_def (name, prop) =
     1.8 -  Theory.add_defs_i false false [(name, prop)] #>
     1.9 -  (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
    1.10 -
    1.11 -fun add_def_new (name, prop) thy =  (* FIXME inactive --- breaks codegen *)
    1.12 +fun add_def (name, prop) thy =
    1.13    let
    1.14      val tfrees = rev (map TFree (Term.add_tfrees prop []));
    1.15      val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length tfrees));
    1.16 @@ -224,8 +220,8 @@
    1.17  
    1.18      val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
    1.19      val thy' = Theory.add_defs_i false false [(name, prop')] thy;
    1.20 -    val axm = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    1.21 -    val def = Thm.instantiate (recover_sorts, []) axm;
    1.22 +    val axm' = Thm.get_axiom_i thy' (Sign.full_name thy' name);
    1.23 +    val def = Thm.instantiate (recover_sorts, []) axm';
    1.24    in (Drule.unvarify def, thy') end;
    1.25  
    1.26  in