| changeset 19305 | 5c16895d548b |
| parent 19230 | 3342e7554b77 |
| child 19429 | e425e74b01af |
--- a/src/Pure/thm.ML Tue Mar 21 12:18:13 2006 +0100 +++ b/src/Pure/thm.ML Tue Mar 21 12:18:15 2006 +0100 @@ -450,7 +450,7 @@ val concl_of = Logic.strip_imp_concl o prop_of; val prems_of = Logic.strip_imp_prems o prop_of; fun nprems_of th = Logic.count_prems (prop_of th, 0); -val no_prems = equal 0 o nprems_of; +fun no_prems th = nprems_of th = 0; fun major_prem_of th = (case prems_of th of