change for new rewriting

--- a/src/ZF/ex/Term.ML	Thu Jan 13 17:34:59 2000 +0100
+++ b/src/ZF/ex/Term.ML	Thu Jan 13 17:36:02 2000 +0100
@@ -72,7 +72,7 @@
 by (Simp_tac 1);
 by (rtac impI 1);
 by (subgoal_tac "rank(a)<i & rank(l) < i" 1);
-by (asm_simp_tac (simpset() addsimps [VsetI]) 1);
+by (asm_simp_tac (simpset() addsimps [rank_of_Ord]) 1);
 by (full_simp_tac (simpset() addsimps list.con_defs) 1);
 by (blast_tac (claset() addDs (rank_rls RL [lt_trans])) 1);
 qed "map_lemma";
@@ -82,7 +82,7 @@
 \     term_rec(Apply(a,ts), d) = d(a, ts, map (%z. term_rec(z,d), ts))";
 by (rtac (term_rec_def RS def_Vrec RS trans) 1);
 by (rewrite_goals_tac term.con_defs);
-by (asm_simp_tac (simpset() addsimps [Ord_rank, rank_pair2, map_lemma]) 1);;
+by (asm_simp_tac (simpset() addsimps [rank_pair2, map_lemma]) 1);;
 qed "term_rec";
 
 (*Slightly odd typing condition on r in the second premise!*)