--- a/programs/prove1.scala	Tue Nov 12 08:03:16 2013 +0000
+++ b/programs/prove1.scala	Tue Nov 12 09:57:22 2013 +0000
@@ -31,17 +31,18 @@
 
 val goal = Judgement(Gamma, Del) // request: provable or not?
 
+def partitions[A](ls: List[A]): List[(A, List[A])]  = 
+  ls.map (s => (s, ls diff List(s)))
+
+
 def prove(j: Judgement, sc: () => Unit) : Unit = {
   if (j.lhs.contains(j.rhs))  sc()   // Axiom rule 
   else prove1(j.lhs, j.rhs, sc) 
 }
 
-def partitions[A](ls: List[A]): List[(A, List[A])]  = 
-  ls.map (s => (s, ls diff List(s)))
-
 def prove1(lhs: List[Form], rhs: Form, sc: () => Unit) : Unit = 
   rhs match {
-    case True => sc()
+    case True => sc ()
     case False => ()
     case Imp(f1, f2) => prove(Judgement(f1::lhs, f2), sc) 
     case Says(p, f1) => prove(Judgement(lhs, f1), sc)