From 59ee1bfd7c430576427943384f2e52efb9b3da08 Mon Sep 17 00:00:00 2001
From: aarne <aarne@cs.chalmers.se>
Date: Tue, 20 Dec 2005 22:38:38 +0000
Subject: full disjunctive patterns ; more prec levels for Exp

---
 examples/systemS/ProofSymb.gf | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'examples')

diff --git a/examples/systemS/ProofSymb.gf b/examples/systemS/ProofSymb.gf
index 4ff18ca14..3de1b91b7 100644
--- a/examples/systemS/ProofSymb.gf
+++ b/examples/systemS/ProofSymb.gf
@@ -18,7 +18,7 @@ concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in {
     RedAbs form = continue ["Reductio ad absurdum"] (task neg abs)
       where { neg = useTop (prefixR 4 "~" form) } ;
 
-    ExFalso form = finish (["Ex falso quodlibet"] ++ form.s) "Ø" ; --- form
+    ExFalso form = finish (["Ex falso quodlibet"] ++ toProve form) "Ø" ; --- form
 
     ConjSplit a b c = 
       continue ["Conjunction split"] 
@@ -81,4 +81,10 @@ concrete ProofSymb of Proof = FormulaSymb ** open Prelude, Precedence in {
 
     abs = "_|_" ;
  
+    toProve : PrecExp -> Str = \c -> 
+      variants {
+        [] ;      -- for generation
+        useTop c  -- for parsing
+        } ;
+
 }
\ No newline at end of file
-- 
cgit v1.2.3