src/Pure/Isar/object_logic.ML

   val add_judgment_i: bstring * typ * mixfix -> theory -> theory
   val judgment_name: theory -> string
   val is_judgment: theory -> term -> bool
   val drop_judgment: theory -> term -> term
   val fixed_judgment: theory -> string -> term
-  val assert_propT: theory -> term -> term
+  val ensure_propT: theory -> term -> term
   val declare_atomize: theory attribute
   val declare_rulify: theory attribute
   val atomize_term: theory -> term -> term
   val atomize_cterm: theory -> cterm -> thm
   val atomize_thm: thm -> thm

       if_none (Sign.const_type thy c) (aT --> propT)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;
 
-fun assert_propT thy t =
+fun ensure_propT thy t =
   let val T = Term.fastype_of t
   in if T = propT then t else Const (judgment_name thy, T --> propT) $ t end;