src/Pure/Syntax/syntax.ML
changeset 24512 fc4959967b30
parent 24488 646e782ba8ff
child 24613 bc889c3d55a3
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sat Sep 01 15:47:04 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sat Sep 01 15:47:05 2007 +0200
     1.3 @@ -100,6 +100,9 @@
     1.4    val global_parse_term: theory -> string -> term
     1.5    val global_parse_prop: theory -> string -> term
     1.6    val check_sort: Proof.context -> sort -> sort
     1.7 +  val check_typ: Proof.context -> typ -> typ
     1.8 +  val check_term: Proof.context -> term -> term
     1.9 +  val check_prop: Proof.context -> term -> term
    1.10    val check_typs: Proof.context -> typ list -> typ list
    1.11    val check_terms: Proof.context -> term list -> term list
    1.12    val check_props: Proof.context -> term list -> term list
    1.13 @@ -671,8 +674,11 @@
    1.14  
    1.15  val check_typs = gen_check fst (op =);
    1.16  val check_terms = gen_check snd (op aconv);
    1.17 +fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;
    1.18  
    1.19 -fun check_props ctxt = map (fn t => TypeInfer.constrain t propT) #> check_terms ctxt;
    1.20 +val check_typ = singleton o check_typs;
    1.21 +val check_term = singleton o check_terms;
    1.22 +val check_prop = singleton o check_props;
    1.23  
    1.24  fun check_sort ctxt S =
    1.25    (case singleton (check_typs ctxt) (TFree ("", S)) of   (* FIXME TypeInfer.invent_type (!?) *)