# HG changeset patch
# User wenzelm
# Date 1632246150 -7200
# Node ID 1c2c0380d58b7881919be494c165a7807c35e043
# Parent  e0c072a1377121b008bdb93a649a034391e30b7a
clarified partial application: immediate check of object-logic, and avoidance of context within closure;

diff -r e0c072a13771 -r 1c2c0380d58b src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Tue Sep 21 16:23:33 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML	Tue Sep 21 19:42:30 2021 +0200
@@ -122,13 +122,17 @@
     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 is_judgment ctxt =
+  let val name = judgment_name ctxt
+  in fn Const (c, _) $ _ => c = name | _ => false end;
 
-fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
-  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
-      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
-  | drop_judgment _ tm = tm;
+fun drop_judgment ctxt =
+  let
+    val name = judgment_name ctxt;
+    fun drop (Abs (x, T, t)) = Abs (x, T, drop t)
+      | drop (t as Const (c, _) $ u) = if c = name then u else t
+      | drop t = t;
+  in drop end handle TERM _ => I;
 
 fun fixed_judgment ctxt x =
   let  (*be robust wrt. low-level errors*)
diff -r e0c072a13771 -r 1c2c0380d58b src/Pure/ML/ml_antiquotations1.ML
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 21 16:23:33 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 21 19:42:30 2021 +0200
@@ -198,12 +198,19 @@
 
 (* object-logic judgment *)
 
-fun make_judgment ctxt t = Const (Object_Logic.judgment_const ctxt) $ t;
+fun make_judgment ctxt =
+  let val const = Object_Logic.judgment_const ctxt
+  in fn t => Const const $ t end;
 
-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]);
+fun dest_judgment ctxt =
+  let
+    val is_judgment = Object_Logic.is_judgment ctxt;
+    val drop_judgment = Object_Logic.drop_judgment ctxt;
+  in
+    fn t =>
+      if is_judgment t then drop_judgment t
+      else raise TERM ("dest_judgment", [t])
+  end;
 
 val _ = Theory.setup
  (ML_Antiquotation.value \<^binding>\<open>make_judgment\<close>