diff -r d20a9dd2a68c -r 89103008502f src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Oct 21 18:17:00 2005 +0200
+++ b/src/Pure/goal.ML	Fri Oct 21 18:20:29 2005 +0200
@@ -36,8 +36,8 @@
 (* managing goal states *)
 
 (*
-  ----------------- (init)
-  Goal C ==> Goal C
+  ------------ (init)
+  C ==> Goal C
 *)
 fun init ct = Drule.instantiate' [] [SOME ct] Drule.goalI;
 
@@ -56,7 +56,7 @@
   Goal C
   ------ (finish)
     C
-*)  
+*)
 fun finish th =
   (case Thm.nprems_of th of
     0 => conclude th
@@ -67,7 +67,7 @@
 
 (* prove_raw -- minimal checks, no normalization *)
 
-fun prove_raw thy goal tac =  
+fun prove_raw thy goal tac =
   (case SINGLE tac (init (Thm.cterm_of thy goal)) of
     SOME th => finish th
   | NONE => raise ERROR_MESSAGE "Tactic failed.");
@@ -157,7 +157,6 @@
     else Seq.empty
   end;
 
-
 end;
 
 structure BasicGoal: BASIC_GOAL = Goal;