# 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