| changeset 46214 | 8534f949548e |
| parent 42279 | 6da43a5018e2 |
| child 56245 | 84fc7dfa3cd4 |
--- a/src/Pure/Syntax/simple_syntax.ML Sat Jan 14 16:25:54 2012 +0100 +++ b/src/Pure/Syntax/simple_syntax.ML Sat Jan 14 16:58:29 2012 +0100 @@ -101,8 +101,7 @@ val bind = idt --| $$ "."; fun term env T x = - ($$ "!!" |-- bind :|-- (fn v => - term (v :: env) propT >> (fn B => Term.all (#2 v) $ lambda (Free v) B)) || + ($$ "!!" |-- bind :|-- (fn v => term (v :: env) propT >> (Logic.all (Free v))) || term1 env T) x and term1 env T x = (enum2 "==>" (term2 env propT) >> foldr1 Logic.mk_implies ||