src/HOL/W0/W0.thy
changeset 15236 f289e8ba2bb3
parent 15140 322485b816ac
child 19380 b808efaa5828
     1.1 --- a/src/HOL/W0/W0.thy	Mon Oct 11 07:39:19 2004 +0200
     1.2 +++ b/src/HOL/W0/W0.thy	Mon Oct 11 07:42:22 2004 +0200
     1.3 @@ -890,7 +890,7 @@
     1.4    apply (tactic "safe_tac HOL_cs")
     1.5      apply (bestsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
     1.6     apply (fastsimp dest: sym [THEN W_var_geD] new_tv_subst_le new_tv_list_le)
     1.7 -  apply (drule_tac e = expr1 in sym [THEN W_var_geD])
     1.8 +  apply (drule_tac e = e1 in sym [THEN W_var_geD])
     1.9    apply (drule new_tv_subst_tel, assumption)
    1.10    apply (drule_tac ts = "$s a" in new_tv_list_le, assumption)
    1.11    apply (drule new_tv_subst_tel, assumption)