src/Pure/sign.ML

   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_syntax: theory -> typ -> typ
   val certify_typ_abbrev: theory -> typ -> typ
   val certify_term: Pretty.pp -> theory -> term -> term * typ * int
+  val certify_prop: Pretty.pp -> theory -> term -> term * typ * int
+  val cert_term: theory -> term -> term
+  val cert_prop: theory -> term -> term
   val read_sort': Syntax.syntax -> theory -> string -> sort
   val read_sort: theory -> string -> sort
   val read_typ': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
   val read_typ_syntax': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ
   val read_typ_abbrev': Syntax.syntax -> theory * (indexname -> sort option) -> string -> typ

     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val read_def_terms:
     theory * (indexname -> typ option) * (indexname -> sort option) ->
     string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val simple_read_term: theory -> typ -> string -> term
+  val read_term: theory -> string -> term
+  val read_prop: theory -> string -> term
   val const_of_class: class -> string
   val class_of_const: string -> class
   include SIGN_THEORY
 end
 

     check_atoms tm';
     (tm', type_check pp tm', maxidx_of_term tm')
   end;
 
 end;
+
+fun certify_prop pp thy tm =
+  let val res as (tm', T, _) = certify_term pp thy tm
+  in if T <> propT then raise TYPE ("Term not of type prop", [T], [tm']) else res end;
+
+fun cert_term thy tm = #1 (certify_term (pp thy) thy tm);
+fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm);
 
 
 
 (** read and certify entities **)    (*exception ERROR*)
 

 
 fun infer_types pp thy def_type def_sort used freeze tsT =
   apfst hd (infer_types_simult pp thy def_type def_sort used freeze [tsT]);
 
 
-
-(** read_def_terms -- read terms and infer types **)    (*exception ERROR*)
+(* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
 
 fun read_def_terms' pp is_logtype syn (thy, types, sorts) used freeze sTs =
   let
     fun read (s, T) =
       let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg

 
 fun simple_read_term thy T s =
   let val ([t], _) = read_def_terms (thy, K NONE, K NONE) [] true [(s, T)]
   in t end
   handle ERROR => error ("The error(s) above occurred for term " ^ s);
+
+fun read_term thy = simple_read_term thy TypeInfer.logicT;
+fun read_prop thy = simple_read_term thy propT;
 
 
 
 (** signature extension functions **)  (*exception ERROR/TYPE*)