src/ZF/ex/Term.ML

--- a/src/ZF/ex/Term.ML	Wed Jan 08 15:03:53 1997 +0100
+++ b/src/ZF/ex/Term.ML	Wed Jan 08 15:04:27 1997 +0100
@@ -11,7 +11,7 @@
 
 goal Term.thy "term(A) = A * list(term(A))";
 let open term;  val rew = rewrite_rule con_defs in  
-by (fast_tac (sum_cs addSIs (equalityI :: map rew intrs)
+by (fast_tac (!claset addSIs (equalityI :: map rew intrs)
                      addEs [rew elim]) 1)
 end;
 qed "term_unfold";