src/HOL/Tools/res_axioms.ML
changeset 27330 1af2598b5f7d
parent 27194 d4036ec60d46
child 27809 a1e409db516b
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Mon Jun 23 20:00:58 2008 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Mon Jun 23 23:45:39 2008 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4                      (*Forms a lambda-abstraction over the formal parameters*)
     1.5              val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
     1.6              val cdef = cname ^ "_def"
     1.7 -            val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
     1.8 +            val thy'' = Theory.add_defs_i true false [(cdef, Logic.mk_equals (c, rhs))] thy'
     1.9              val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
    1.10            in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
    1.11        | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
    1.12 @@ -113,7 +113,7 @@
    1.13                  val rhs = list_abs_free (map dest_Free args,
    1.14                                           HOLogic.choice_const T $ xtp)
    1.15                        (*Forms a lambda-abstraction over the formal parameters*)
    1.16 -                val def = equals cT $ c $ rhs
    1.17 +                val def = Logic.mk_equals (c, rhs)
    1.18              in dec_sko (subst_bound (list_comb(c,args), p))
    1.19                         (def :: defs)
    1.20              end