src/HOL/Tools/res_axioms.ML
changeset 28674 08a77c495dc1
parent 28544 26743a1591f5
child 28965 1de908189869
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4                Sign.declare_const [Markup.property_internal] ((Name.binding cname, cT), NoSyn) thy
     1.5              val cdef = cname ^ "_def"
     1.6              val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
     1.7 -            val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
     1.8 +            val ax = Thm.axiom thy'' (Sign.full_name thy'' cdef)
     1.9            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
    1.10        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
    1.11            (*Universal quant: insert a free variable into body and continue*)