--- a/src/Cube/Cube.thy Fri Dec 17 17:08:56 2010 +0100
+++ b/src/Cube/Cube.thy Fri Dec 17 17:43:54 2010 +0100
@@ -14,8 +14,7 @@
typedecl "context"
typedecl typing
-nonterminals
- context' typing'
+nonterminal context' and typing'
consts
Abs :: "[term, term => term] => term"