# HG changeset patch
# User wenzelm
# Date 1269695437 -3600
# Node ID 87e6e2737aee1ec600a6b930bd4810832157ee49
# Parent  27e2fa7d4ce7fa3366a58f2cacb8516631782f79
eliminated old-style Theory.add_defs_i;

diff -r 27e2fa7d4ce7 -r 87e6e2737aee src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 27 02:10:00 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sat Mar 27 14:10:37 2010 +0100
@@ -91,10 +91,10 @@
             val (c, thy') =
               Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
             val cdef = cname ^ "_def"
-            val thy'' =
-              Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
-            val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
-          in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
+            val (ax, thy'') =
+              Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
+            val ax' = Drule.export_without_context ax
+          in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
       | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
           let val fname = Name.variant (OldTerm.add_term_names (p, [])) a