src/Pure/Isar/expression.ML
changeset 33173 b8ca12f6681a
parent 33040 cffdb7b28498
child 33278 ba9f52f56356
     1.1 --- a/src/Pure/Isar/expression.ML	Sun Oct 25 20:54:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Sun Oct 25 21:35:46 2009 +0100
     1.3 @@ -639,7 +639,7 @@
     1.4      val ([pred_def], defs_thy) =
     1.5        thy
     1.6        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
     1.7 -      |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
     1.8 +      |> Sign.declare_const ((bname, predT), NoSyn) |> snd
     1.9        |> PureThy.add_defs false
    1.10          [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
    1.11      val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;