--- a/src/Pure/Isar/expression.ML Sun Oct 25 20:54:21 2009 +0100
+++ b/src/Pure/Isar/expression.ML Sun Oct 25 21:35:46 2009 +0100
@@ -639,7 +639,7 @@
val ([pred_def], defs_thy) =
thy
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
- |> Sign.declare_const [] ((bname, predT), NoSyn) |> snd
+ |> Sign.declare_const ((bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
[((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;