changeset 1906 | 4699a9058a4f |
parent 1756 | 978ee7ededdd |
child 2004 | 3411fe560611 |
--- a/src/Pure/drule.ML Mon Aug 12 16:26:02 1996 +0200 +++ b/src/Pure/drule.ML Mon Aug 12 16:28:15 1996 +0200 @@ -137,7 +137,7 @@ val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); in if not (forall is_Free args) then - err "Arguments of lhs have to be variables" + err "Arguments (on lhs) must be variables" else if not (null lhs_dups) then err ("Duplicate variables on lhs: " ^ show_frees lhs_dups) else if not (null rhs_extras) then