author | paulson |
Mon, 12 Aug 1996 16:28:15 +0200 | |
changeset 1906 | 4699a9058a4f |
parent 1905 | 81061bd61ad3 |
child 1907 | d069f23e941f |
src/Pure/drule.ML | file | annotate | diff | comparison | revisions |
--- 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