ex/PL.ML

--- a/ex/PL.ML	Tue Mar 22 19:54:55 1994 +0100
+++ b/ex/PL.ML	Tue Mar 22 19:55:29 1994 +0100
@@ -135,8 +135,7 @@
 
 (** The function eval **)
 
-val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp]
-                            @ PL0.inject @ PL0.ineq;
+val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp] @ PL0.simps;
 
 goalw PL.thy [eval_def] "tt[false] = False";
 by (simp_tac pl_ss 1);