diff -r d0f6c33b2300 -r 6961e8ab33e1 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Jun 20 22:14:07 2005 +0200
+++ b/src/Pure/sign.ML	Mon Jun 20 22:14:08 2005 +0200
@@ -133,6 +133,9 @@
   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
@@ -156,6 +159,8 @@
     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
@@ -464,6 +469,13 @@
 
 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*)
@@ -575,8 +587,7 @@
   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
@@ -593,6 +604,9 @@
   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*)