| changeset 24680 | 0d355aa59e67 |
| parent 24613 | bc889c3d55a3 |
| child 24709 | ecfb9dcb6c4c |
--- a/src/Pure/Syntax/syntax.ML Sun Sep 23 22:23:24 2007 +0200 +++ b/src/Pure/Syntax/syntax.ML Sun Sep 23 22:23:27 2007 +0200 @@ -674,7 +674,7 @@ val check_typs = gen_check fst (op =); val check_terms = gen_check snd (op aconv); -fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt; +fun check_props ctxt = map (TypeInfer.constrain propT) #> check_terms ctxt; val check_typ = singleton o check_typs; val check_term = singleton o check_terms;