removed redundant Sign.certify_prop, use Sign.cert_prop instead;
tuned;

--- a/src/Pure/sign.ML	Wed Sep 30 22:26:47 2009 +0200
+++ b/src/Pure/sign.ML	Wed Sep 30 22:27:20 2009 +0200
@@ -68,7 +68,6 @@
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
   val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
   val certify_term: theory -> term -> term * typ * int
-  val certify_prop: theory -> term -> term * typ * int
   val cert_term: theory -> term -> term
   val cert_prop: theory -> term -> term
   val no_frees: Pretty.pp -> term -> term
@@ -369,11 +368,9 @@
   in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
 
 fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
-fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
-
 fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
 val cert_term = #1 oo certify_term;
-val cert_prop = #1 oo certify_prop;
+fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
 
 end;
 

--- a/src/Pure/theory.ML	Wed Sep 30 22:26:47 2009 +0200
+++ b/src/Pure/theory.ML	Wed Sep 30 22:27:20 2009 +0200
@@ -94,7 +94,8 @@
   val empty = make_thy (NameSpace.empty_table, Defs.empty, ([], []));
   val copy = I;
 
-  fun extend (Thy {axioms, defs, wrappers}) = make_thy (NameSpace.empty_table, defs, wrappers);
+  fun extend (Thy {axioms = _, defs, wrappers}) =
+    make_thy (NameSpace.empty_table, defs, wrappers);
 
   fun merge pp (thy1, thy2) =
     let
@@ -155,7 +156,7 @@
 
 fun cert_axm thy (b, raw_tm) =
   let
-    val (t, T, _) = Sign.certify_prop thy raw_tm
+    val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
   in