diff -r 5f99df1e26c4 -r 18d44ab74672 ex/PL.ML
--- a/ex/PL.ML	Sat Aug 13 16:33:53 1994 +0200
+++ b/ex/PL.ML	Sat Aug 13 16:34:30 1994 +0200
@@ -135,7 +135,9 @@
 
 (** The function eval **)
 
-val pl_ss = set_ss addsimps [pl_rec_var,pl_rec_false,pl_rec_imp] @ PL.pl.simps;
+val pl_ss = set_ss addsimps
+  (PL.pl.simps @ [eval2_false, eval2_var, eval2_imp]
+               @ [hyps_false, hyps_var, hyps_imp]);
 
 goalw PL.thy [eval_def] "tt[false] = False";
 by (simp_tac pl_ss 1);
@@ -151,22 +153,6 @@
 
 val pl_ss = pl_ss addsimps [eval_false, eval_var, eval_imp];
 
-(** The function hyps **)
-
-goalw PL.thy [hyps_def] "hyps(false,tt) = {}";
-by (simp_tac pl_ss 1);
-val hyps_false = result();
-
-goalw PL.thy [hyps_def] "hyps(#v,tt) = {if(v:tt, #v, #v->false)}";
-by (simp_tac pl_ss 1);
-val hyps_var = result();
-
-goalw PL.thy [hyps_def] "hyps(p->q,tt) = hyps(p,tt) Un hyps(q,tt)";
-by (simp_tac pl_ss 1);
-val hyps_imp = result();
-
-val pl_ss = pl_ss addsimps [hyps_false, hyps_var, hyps_imp];
-
 val ball_eq = prove_goalw Set.thy [Ball_def] "(!x:A.P(x)) = (!x.x:A --> P(x))"
 	(fn _ => [rtac refl 1]);