# HG changeset patch
# User wenzelm
# Date 1188479089 -7200
# Node ID e92b74b3a254703124701b745d0059f41fa6d2f2
# Parent  1dbf377c2e9a9e23b25147dc7d3f19283bf2685d
tuned;

diff -r 1dbf377c2e9a -r e92b74b3a254 src/Pure/Syntax/simple_syntax.ML
--- 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;