src/ZF/listfn.ML
changeset 25 3ac1c0c0016e
parent 14 1c0926788772
--- a/src/ZF/listfn.ML	Tue Oct 05 13:15:01 1993 +0100
+++ b/src/ZF/listfn.ML	Tue Oct 05 15:21:29 1993 +0100
@@ -59,7 +59,7 @@
 
 goal ListFn.thy "list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))";
 by (rtac (list_rec_def RS def_Vrec RS trans) 1);
-by (simp_tac (ZF_ss addsimps (List.case_eqns @ [Vset_rankI, rank_Cons2])) 1);
+by (simp_tac (rank_ss addsimps (rank_Cons2::List.case_eqns)) 1);
 val list_rec_Cons = result();
 
 (*Type checking -- proved by induction, as usual*)