tidying

--- a/src/FOL/ex/If.ML	Thu Jul 16 11:50:01 1998 +0200
+++ b/src/FOL/ex/If.ML	Thu Jul 16 12:10:56 1998 +0200
@@ -9,20 +9,19 @@
 open If;
 open Cla;    (*in case structure IntPr is open!*)
 
-val prems = goalw If.thy [if_def]
+val prems = Goalw [if_def]
     "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)";
 by (blast_tac (claset() addIs prems) 1);
 qed "ifI";
 
-val major::prems = goalw If.thy [if_def]
+val major::prems = Goalw [if_def]
    "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S";
 by (cut_facts_tac [major] 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "ifE";
 
 
-Goal
-    "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
+Goal "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
 by (rtac iffI 1);
 by (etac ifE 1);
 by (etac ifE 1);