src/Pure/Isar/expression.ML
changeset 35238 18ae6ef02fe0
parent 35204 214ec053128e
child 35262 9ea4445d2ccf
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Feb 19 20:39:48 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Feb 19 20:41:34 2010 +0100
     1.3 @@ -641,8 +641,7 @@
     1.4        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
     1.5        |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
     1.6        |> PureThy.add_defs false
     1.7 -        [((Binding.conceal (Binding.map_name Thm.def_name binding),
     1.8 -            Logic.mk_equals (head, body)), [])];
     1.9 +        [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
    1.10      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
    1.11  
    1.12      val cert = Thm.cterm_of defs_thy;