src/HOL/Sexp.ML
changeset 4059 59c1422c9da5
parent 3029 db0e9b30dc92
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Sexp.ML	Sat Nov 01 12:58:08 1997 +0100
     1.2 +++ b/src/HOL/Sexp.ML	Sat Nov 01 12:59:06 1997 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4  goal Sexp.thy "wf(pred_sexp)";
     1.5  by (rtac (pred_sexp_subset_Sigma RS wfI) 1);
     1.6  by (etac sexp.induct 1);
     1.7 -by (ALLGOALS (fast_tac (!claset addSEs [mp, pred_sexpE])));
     1.8 +by (ALLGOALS (blast_tac (!claset addSEs [allE, pred_sexpE])));
     1.9  qed "wf_pred_sexp";
    1.10  
    1.11