clarified partial application: immediate check of object-logic, and avoidance of context within closure;
--- 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*)
--- 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>