# HG changeset patch
# User paulson
# Date 835107524 -7200
# Node ID 9083542fd8614426abe0fd9d32795edf5f34601e
# Parent  0eef167ebe1bd0d803390064ed3431ea0dd00406
Removal of list_all

diff -r 0eef167ebe1b -r 9083542fd861 src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Tue Jun 18 16:17:38 1996 +0200
+++ b/src/HOL/ex/Term.ML	Tue Jun 18 16:18:44 1996 +0200
@@ -65,7 +65,7 @@
 
 (*Induction for the abstract type 'a term*)
 val prems = goalw Term.thy [App_def,Rep_Tlist_def,Abs_Tlist_def]
-    "[| !!x ts. list_all R ts ==> R(App x ts)  \
+    "[| !!x ts. (ALL t: setOfList ts. R t) ==> R(App x ts)  \
 \    |] ==> R(t)";
 by (rtac (Rep_term_inverse RS subst) 1);   (*types force good instantiation*)
 by (res_inst_tac [("P","Rep_term(t) : sexp")] conjunct2 1);
@@ -86,8 +86,8 @@
 by (etac conjunct1 2);
 by (etac rev_subsetD 2);
 by (rtac list_subset_sexp 2);
-by (fast_tac set_cs 2);
 by (ALLGOALS Asm_simp_tac);
+by (ALLGOALS Fast_tac);
 qed "term_induct";
 
 (*Induction for the abstract type 'a term*)