src/Pure/Isar/object_logic.ML

   val get_base_sort: Proof.context -> sort option
   val add_base_sort: sort -> theory -> theory
   val add_judgment: binding * typ * mixfix -> theory -> theory
   val add_judgment_cmd: binding * string * mixfix -> theory -> theory
   val judgment_name: Proof.context -> string
+  val judgment_const: Proof.context -> string * typ
   val is_judgment: Proof.context -> term -> bool
   val drop_judgment: Proof.context -> term -> term
   val fixed_judgment: Proof.context -> string -> term
   val ensure_propT: Proof.context -> term -> term
   val dest_judgment: Proof.context -> cterm -> cterm

 fun judgment_name ctxt =
   (case #judgment (get_data ctxt) of
     SOME name => name
   | _ => raise TERM ("Unknown object-logic judgment", []));
 
+fun judgment_const ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val c = judgment_name ctxt;
+    val T = Sign.the_const_type thy c;
+  in (c, T) end;
+
 fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
   | is_judgment _ _ = false;
 
 fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
   | drop_judgment ctxt (tm as (Const (c, _) $ t)) =