# HG changeset patch
# User wenzelm
# Date 1632222734 -7200
# Node ID edf8b141a8c4ec45561950c551f3e6c1d0658837
# Parent  e098fa45bfe037ef75185526f7f72f93d08a0593
ML antiquotations for object-logic judgment;

diff -r e098fa45bfe0 -r edf8b141a8c4 NEWS
--- a/NEWS	Tue Sep 21 12:35:38 2021 +0200
+++ b/NEWS	Tue Sep 21 13:12:14 2021 +0200
@@ -262,6 +262,10 @@
 * ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
 corresponding ML values, notably as arguments for Thm.instantiate etc.
 
+* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
+corresponding functions for the object-logic of the ML compilation
+context. This supersedes older mk_Trueprop / dest_Trueprop operations.
+
 * ML antiquotations for type constructors and term constants:
 
     \<^Type>\<open>c\<close>
diff -r e098fa45bfe0 -r edf8b141a8c4 etc/symbols
--- a/etc/symbols	Tue Sep 21 12:35:38 2021 +0200
+++ b/etc/symbols	Tue Sep 21 13:12:14 2021 +0200
@@ -456,6 +456,8 @@
 \<^ctyp>                argument: cartouche
 \<^keyword>             argument: cartouche
 \<^locale>              argument: cartouche
+\<^make_judgment>
+\<^dest_judgment>
 \<^make_string>
 \<^method>              argument: cartouche
 \<^named_theorems>      argument: cartouche
diff -r e098fa45bfe0 -r edf8b141a8c4 lib/texinputs/isabellesym.sty
--- a/lib/texinputs/isabellesym.sty	Tue Sep 21 12:35:38 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Tue Sep 21 13:12:14 2021 +0200
@@ -446,6 +446,8 @@
 \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
 \newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
 \newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
+\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
 \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
 \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
 \newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
diff -r e098fa45bfe0 -r edf8b141a8c4 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Sep 21 12:35:38 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Sep 21 13:12:14 2021 +0200
@@ -11,6 +11,7 @@
   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
@@ -114,6 +115,13 @@
     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;
 
diff -r e098fa45bfe0 -r edf8b141a8c4 src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 21 12:35:38 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 21 13:12:14 2021 +0200
@@ -4,7 +4,13 @@
 Miscellaneous ML antiquotations: part 1.
 *)
 
-structure ML_Antiquotations1: sig end =
+signature ML_ANTIQUOTATIONS1 =
+sig
+  val make_judgment: Proof.context -> term -> term
+  val dest_judgment: Proof.context -> term -> term
+end;
+
+structure ML_Antiquotations1: ML_ANTIQUOTATIONS1 =
 struct
 
 (* ML support *)
@@ -190,6 +196,22 @@
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
 
+(* object-logic judgment *)
+
+fun make_judgment ctxt t = Const (Object_Logic.judgment_const ctxt) $ t;
+
+fun dest_judgment ctxt t =
+  if Object_Logic.is_judgment ctxt t
+  then Object_Logic.drop_judgment ctxt t
+  else raise TERM ("dest_judgment", [t]);
+
+val _ = Theory.setup
+ (ML_Antiquotation.value \<^binding>\<open>make_judgment\<close>
+   (Scan.succeed "ML_Antiquotations1.make_judgment ML_context") #>
+  ML_Antiquotation.value \<^binding>\<open>dest_judgment\<close>
+   (Scan.succeed "ML_Antiquotations1.dest_judgment ML_context"));
+
+
 (* type/term constructors *)
 
 local