tuned;

--- a/src/Pure/Syntax/simple_syntax.ML	Thu Aug 30 15:04:48 2007 +0200
+++ b/src/Pure/Syntax/simple_syntax.ML	Thu Aug 30 15:04:49 2007 +0200
@@ -109,8 +109,6 @@
 val idt = ident -- constraint;
 val bind = idt --| $$ ".";
 
-in
-
 fun term env T x =
  ($$ "!!" |-- bind :|-- (fn v =>
    term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) ||
@@ -146,6 +144,8 @@
     else error ("Unspecified types in input: " ^ quote s)
   end;
 
+in
+
 val read_term = read_tm dummyT;
 val read_prop = read_tm propT;