diff -r d069f23e941f -r 55d8e38262a8 src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Fri Aug 16 11:27:10 1996 +0200
+++ b/src/HOL/ex/Term.ML	Mon Aug 19 11:12:38 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. (ALL t: setOfList ts. R t) ==> R(App x ts)  \
+    "[| !!x ts. (ALL t: set_of_list 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);