src/Pure/sign.ML
changeset 32789 d89327de0b3c
parent 31946 99ac0321cd47
child 33095 bbd52d2f8696
     1.1 --- a/src/Pure/sign.ML	Wed Sep 30 22:26:47 2009 +0200
     1.2 +++ b/src/Pure/sign.ML	Wed Sep 30 22:27:20 2009 +0200
     1.3 @@ -68,7 +68,6 @@
     1.4    val certify_typ_mode: Type.mode -> theory -> typ -> typ
     1.5    val certify': bool -> Pretty.pp -> bool -> Consts.T -> theory -> term -> term * typ * int
     1.6    val certify_term: theory -> term -> term * typ * int
     1.7 -  val certify_prop: theory -> term -> term * typ * int
     1.8    val cert_term: theory -> term -> term
     1.9    val cert_prop: theory -> term -> term
    1.10    val no_frees: Pretty.pp -> term -> term
    1.11 @@ -369,11 +368,9 @@
    1.12    in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
    1.13  
    1.14  fun certify_term thy = certify' false (Syntax.pp_global thy) true (consts_of thy) thy;
    1.15 -fun certify_prop thy = certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
    1.16 -
    1.17  fun cert_term_abbrev thy = #1 o certify' false (Syntax.pp_global thy) false (consts_of thy) thy;
    1.18  val cert_term = #1 oo certify_term;
    1.19 -val cert_prop = #1 oo certify_prop;
    1.20 +fun cert_prop thy = #1 o certify' true (Syntax.pp_global thy) true (consts_of thy) thy;
    1.21  
    1.22  end;
    1.23