diff -r 3df60299a6d0 -r 0ed8bdd883e0 src/HOL/Prolog/Test.ML
--- a/src/HOL/Prolog/Test.ML	Thu Dec 13 12:33:23 2001 +0100
+++ b/src/HOL/Prolog/Test.ML	Thu Dec 13 15:45:03 2001 +0100
@@ -1,7 +1,7 @@
 open Test;
 
 val prog_Test = prog_HOHH@[append, reverse, mappred, mapfun, age, eq, bag_appl];
-fun pgoal s = (case Goal s of _ => by(prolog_tac prog_Test));
+fun pgoal s = (case Goal s of _ => by (prolog_tac prog_Test));
 val p = ptac prog_Test 1;
 
 pgoal "append ?x ?y [a,b,c,d]";
@@ -40,8 +40,8 @@
 
 (*
 goal thy "f a = ?g a a & ?g = x"; 
-by(rtac conjI 1);
-by(rtac refl 1);
+by (rtac conjI 1);
+by (rtac refl 1);
 back();
 back();
 *)
@@ -103,19 +103,19 @@
 
 (* implication and disjunction in atom: *)
 goal thy "? Q. (!p q. R(q :- p) => R(Q p q)) & Q (t | s) (s | t)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
 
 (* disjunction in atom: *)
 goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(step_tac HOL_cs 1);
-by(fast_tac HOL_cs 2);
-by(fast_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (step_tac HOL_cs 1);
+by (fast_tac HOL_cs 2);
+by (fast_tac HOL_cs 1);
 (*
 hangs:
 goal thy "(!P. g P :- (P => b | a)) => g(a | b)";
-by(fast_tac HOL_cs 1);
+by (fast_tac HOL_cs 1);
 *)
 
 pgoal "!Emp Stk.(\