--- a/src/Pure/Isar/proof_context.ML Tue Jan 09 15:14:49 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML Tue Jan 09 16:04:21 2024 +0100
@@ -629,8 +629,8 @@
local
fun certify_consts ctxt =
- Consts.certify (Context.Proof ctxt) (tsig_of ctxt)
- (not (abbrev_mode ctxt)) (consts_of ctxt);
+ Consts.certify {do_expand = not (abbrev_mode ctxt)}
+ (Context.Proof ctxt) (tsig_of ctxt) (consts_of ctxt);
fun expand_binds ctxt =
let
@@ -809,17 +809,16 @@
local
-fun gen_cert prop ctxt t =
- t
- |> expand_abbrevs ctxt
- |> (fn t' =>
- #1 (Sign.certify' prop (Context.Proof ctxt) false (consts_of ctxt) (theory_of ctxt) t')
- handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg);
+fun cert_flags flags ctxt t =
+ let val t' = expand_abbrevs ctxt t in
+ #1 (Sign.certify_flags flags (Context.Proof ctxt) (consts_of ctxt) (theory_of ctxt) t')
+ handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg
+ end;
in
-val cert_term = gen_cert false;
-val cert_prop = gen_cert true;
+val cert_term = cert_flags {prop = false, do_expand = false};
+val cert_prop = cert_flags {prop = true, do_expand = false};
end;
--- a/src/Pure/consts.ML Tue Jan 09 15:14:49 2024 +0100
+++ b/src/Pure/consts.ML Tue Jan 09 16:04:21 2024 +0100
@@ -28,7 +28,7 @@
val intern: T -> xstring -> string
val intern_syntax: T -> xstring -> string
val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list
- val certify: Context.generic -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*)
+ val certify: {do_expand: bool} -> Context.generic -> Type.tsig -> T -> term -> term (*exception TYPE*)
val typargs: T -> string * typ -> typ list
val instance: T -> string * typ list -> typ
val dummy_types: T -> term -> term
@@ -164,7 +164,7 @@
(* certify *)
-fun certify context tsig do_expand consts =
+fun certify {do_expand} context tsig consts =
let
fun err msg (c, T) =
raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
@@ -293,8 +293,8 @@
fun abbreviate context tsig mode (b, raw_rhs) consts =
let
- val cert_term = certify context tsig false consts;
- val expand_term = certify context tsig true consts;
+ val cert_term = certify {do_expand = false} context tsig consts;
+ val expand_term = certify {do_expand = true} context tsig consts;
val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
--- a/src/Pure/sign.ML Tue Jan 09 15:14:49 2024 +0100
+++ b/src/Pure/sign.ML Tue Jan 09 16:04:21 2024 +0100
@@ -64,7 +64,8 @@
val certify_sort: theory -> sort -> sort
val certify_typ: theory -> typ -> typ
val certify_typ_mode: Type.mode -> theory -> typ -> typ
- val certify': bool -> Context.generic -> bool -> Consts.T -> theory -> term -> term * typ * int
+ val certify_flags: {prop: bool, do_expand: bool} -> Context.generic -> Consts.T -> theory ->
+ term -> term * typ * int
val certify_term: theory -> term -> term * typ * int
val cert_term: theory -> term -> term
val cert_prop: theory -> term -> term
@@ -304,21 +305,27 @@
in
-fun certify' prop context do_expand consts thy tm =
+fun certify_flags {prop, do_expand} context consts thy tm =
let
val _ = check_vars tm;
val tm' = Term.map_types (certify_typ thy) tm;
val T = type_check context tm';
val _ = if prop andalso T <> propT then err "Term not of type prop" else ();
val tm'' = tm'
- |> Consts.certify context (tsig_of thy) do_expand consts
+ |> Consts.certify {do_expand = do_expand} context (tsig_of thy) consts
|> Soft_Type_System.global_purge thy;
in (if tm = tm'' then tm else tm'', T, Term.maxidx_of_term tm'') end;
-fun certify_term thy = certify' false (Context.Theory thy) true (consts_of thy) thy;
-fun cert_term_abbrev thy = #1 o certify' false (Context.Theory thy) false (consts_of thy) thy;
+fun certify_term thy =
+ certify_flags {prop = false, do_expand = true} (Context.Theory thy) (consts_of thy) thy;
+
+fun cert_term_abbrev thy =
+ #1 o certify_flags {prop = false, do_expand = false} (Context.Theory thy) (consts_of thy) thy;
+
val cert_term = #1 oo certify_term;
-fun cert_prop thy = #1 o certify' true (Context.Theory thy) true (consts_of thy) thy;
+
+fun cert_prop thy =
+ #1 o certify_flags {prop = true, do_expand = true} (Context.Theory thy) (consts_of thy) thy;
end;