--- 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 *)