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