| changeset 29579 | cb520b766e00 |
| parent 27285 | def40a211768 |
| child 29606 | fedb8be05f24 |
--- a/src/Pure/Isar/overloading.ML Wed Jan 21 16:47:03 2009 +0100 +++ b/src/Pure/Isar/overloading.ML Wed Jan 21 16:47:04 2009 +0100 @@ -134,8 +134,8 @@ fun declare c_ty = pair (Const c_ty); -fun define checked name (c, t) = - Thm.add_def (not checked) true (name, Logic.mk_equals (Const (c, Term.fastype_of t), t)); +fun define checked name (c, t) = Thm.add_def (not checked) true (Binding.name name, + Logic.mk_equals (Const (c, Term.fastype_of t), t)); (* target *)