summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 21 Sep 2021 19:42:30 +0200 | |

changeset 74344 | 1c2c0380d58b |

parent 74343 | e0c072a13771 |

child 74345 | e5ff77db6f38 |

clarified partial application: immediate check of object-logic, and avoidance of context within closure;

src/Pure/Isar/object_logic.ML | file | annotate | diff | comparison | revisions | |

src/Pure/ML/ml_antiquotations1.ML | file | annotate | diff | comparison | revisions |

--- 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>