--- a/programs/prove2.scala	Tue Nov 12 09:57:22 2013 +0000
+++ b/programs/prove2.scala	Tue Nov 12 10:51:02 2013 +0000
@@ -37,8 +37,8 @@
 
 val Gamma: Set[Form] = 
   Set( (Admin says Del) -> Del,
-       (Admin says ((Bob says Del) -> Del)),
-       (Bob says Del) )
+       Admin says ((Bob says Del) -> Del),
+       Bob says Del )
 
 val goal = Gamma |- Del // request: provable or not?
 
@@ -48,23 +48,23 @@
 
 def prove(j: Judgement, sc: () => Unit) : Unit = {
   if (j.lhs.contains(j.rhs))  sc ()   // Axiom rule 
-  else prove1(j.lhs, j.rhs, sc) 
+  else prove1(j, sc) 
 }
 
-def prove1(lhs: Set[Form], rhs: Form, sc: () => Unit) : Unit = 
-  rhs match {
+def prove1(j: Judgement, sc: () => Unit) : Unit = 
+  j.rhs match {
     case True => sc ()
     case False => ()
-    case Imp(f1, f2) => prove(lhs + f1 |- f2, sc) 
-    case Says(p, f1) => prove(lhs |- f1, sc) 
+    case Imp(f1, f2) => prove(j.lhs + f1 |- f2, sc) 
+    case Says(p, f1) => prove(j.lhs |- f1, sc) 
     case Or(f1, f2) => 
-      { prove(lhs |- f1, sc);
-        prove(lhs |- f2, sc) }
+      { prove(j.lhs |- f1, sc);
+        prove(j.lhs |- f2, sc) }
     case And(f1, f2) => 
-      prove(lhs |- f1, 
-            () => prove(lhs |- f2, sc))
-    case _ => { for ((f, lhs_rest) <- partitions(lhs))
-                  prove2(f, lhs_rest, rhs, sc) }
+      prove(j.lhs |- f1, 
+            () => prove(j.lhs |- f2, sc))
+    case _ => { for ((f, lhs_rest) <- partitions(j.lhs))
+                  prove2(f, lhs_rest, j.rhs, sc) }
   }
 
 def prove2(f: Form, lhs_rest: Set[Form], rhs: Form, sc: () => Unit) : Unit =