# HG changeset patch
# User paulson
# Date 842460333 -7200
# Node ID 26edb2771d94cc961f3cdc78bfdc002a1a4f7cd9
# Parent  1cff1f4fdb8af5b4a092e80a519966b83dcae572
Removal of univ_cs

diff -r 1cff1f4fdb8a -r 26edb2771d94 src/HOL/Subst/UTerm.ML
--- a/src/HOL/Subst/UTerm.ML	Wed Sep 11 18:40:55 1996 +0200
+++ b/src/HOL/Subst/UTerm.ML	Wed Sep 11 18:45:33 1996 +0200
@@ -13,8 +13,8 @@
 
 goal UTerm.thy "uterm(A) = A <+> A <+> (uterm(A) <*> uterm(A))";
 let val rew = rewrite_rule uterm_con_defs in  
-by (fast_tac (univ_cs addSIs (equalityI :: map rew uterm.intrs)
-                      addEs [rew uterm.elim]) 1)
+by (fast_tac (!claset addSIs (map rew uterm.intrs)
+                      addEs  [rew uterm.elim]) 1)
 end;
 qed "uterm_unfold";
 
@@ -29,7 +29,7 @@
 
 goalw UTerm.thy (uterm_con_defs @ uterm.defs) "uterm(sexp) <= sexp";
 by (rtac lfp_lowerbound 1);
-by (fast_tac (univ_cs addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
+by (fast_tac (!claset addIs sexp.intrs@[sexp_In0I,sexp_In1I]) 1);
 qed "uterm_sexp";
 
 (* A <= sexp ==> uterm(A) <= sexp *)