clarified signature;

--- a/src/Pure/Isar/proof_context.ML	Wed Jan 10 13:43:10 2024 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Jan 10 14:36:29 2024 +0100
@@ -626,7 +626,7 @@
 local
 
 fun certify_consts ctxt =
-  Consts.certify {do_expand = not (abbrev_mode ctxt)}
+  Consts.certify {normalize = not (abbrev_mode ctxt)}
     (Context.Proof ctxt) (tsig_of ctxt) (consts_of ctxt);
 
 fun expand_binds ctxt =
@@ -814,8 +814,8 @@
 
 in
 
-val cert_term = cert_flags {prop = false, do_expand = false};
-val cert_prop = cert_flags {prop = true, do_expand = false};
+val cert_term = cert_flags {prop = false, normalize = false};
+val cert_prop = cert_flags {prop = true, normalize = false};
 
 end;
 

--- a/src/Pure/consts.ML	Wed Jan 10 13:43:10 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 14:36:29 2024 +0100
@@ -29,7 +29,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: {do_expand: bool} -> Context.generic -> Type.tsig -> T -> term -> term  (*exception TYPE*)
+  val certify: {normalize: 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
@@ -50,7 +50,7 @@
 (* datatype T *)
 
 type decl = {T: typ, typargs: int list list};
-type abbrev = {rhs: term, normal_rhs: term, force_expand: bool};
+type abbrev = {rhs: term, normal_rhs: term, internal: bool};
 
 datatype T = Consts of
  {decls: (decl * abbrev option) Name_Space.table,
@@ -169,7 +169,7 @@
 
 (* certify *)
 
-fun certify {do_expand} context tsig consts =
+fun certify {normalize} context tsig consts =
   let
     fun err msg (c, T) =
       raise TYPE (msg ^ " " ^ quote c ^ " :: " ^
@@ -180,7 +180,7 @@
     val need_expand =
       Term.exists_Const (fn (c, _) =>
         (case get_entry consts c of
-          SOME (_, SOME {force_expand, ...}) => do_expand orelse force_expand
+          SOME (_, SOME {internal, ...}) => normalize orelse internal
         | _ => false));
 
     val expand_typ = Type.certify_typ Type.mode_default tsig;
@@ -202,9 +202,9 @@
               if not (Type.raw_instance (T', U)) then err_const (c, T)
               else
                 (case abbr of
-                  SOME {rhs, normal_rhs, force_expand} =>
-                    if do_expand then expand normal_rhs
-                    else if force_expand then expand rhs
+                  SOME {rhs, normal_rhs, internal} =>
+                    if normalize then expand normal_rhs
+                    else if internal then expand rhs
                     else comb head
                 | _ => comb head)
             end
@@ -328,9 +328,9 @@
 
 fun abbreviate context tsig mode (b, raw_rhs) consts =
   let
-    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 cert_term = certify {normalize = false} context tsig consts;
+    val expand_term = certify {normalize = true} context tsig consts;
+    val internal = mode = Print_Mode.internal;
 
     val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
@@ -343,7 +343,7 @@
     consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
       let
         val decl = {T = T, typargs = typargs_of T};
-        val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
+        val abbr = {rhs = rhs, normal_rhs = normal_rhs, internal = internal};
         val _ = Binding.check b;
         val (_, decls') = decls
           |> Name_Space.define context true (b, (decl, SOME abbr));

--- a/src/Pure/sign.ML	Wed Jan 10 13:43:10 2024 +0100
+++ b/src/Pure/sign.ML	Wed Jan 10 14:36:29 2024 +0100
@@ -64,7 +64,7 @@
   val certify_sort: theory -> sort -> sort
   val certify_typ: theory -> typ -> typ
   val certify_typ_mode: Type.mode -> theory -> typ -> typ
-  val certify_flags: {prop: bool, do_expand: bool} -> Context.generic -> Consts.T -> theory ->
+  val certify_flags: {prop: bool, normalize: bool} -> Context.generic -> Consts.T -> theory ->
     term -> term * typ
   val certify_term: theory -> term -> term * typ
   val cert_term: theory -> term -> term
@@ -305,7 +305,7 @@
 
 in
 
-fun certify_flags {prop, do_expand} context consts thy tm =
+fun certify_flags {prop, normalize} context consts thy tm =
   let
     val tsig = tsig_of thy;
     fun check_term t =
@@ -313,7 +313,7 @@
         val _ = check_vars t;
         val t' = Type.certify_types Type.mode_default tsig t;
         val T = type_check context t';
-        val t'' = Consts.certify {do_expand = do_expand} context tsig consts t';
+        val t'' = Consts.certify {normalize = normalize} context tsig consts t';
       in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end;
 
     val (tm1, ty1) = check_term tm;
@@ -322,15 +322,15 @@
   in if tm = tm2 then (tm, ty2) else (tm2, ty2) end;
 
 fun certify_term thy =
-  certify_flags {prop = false, do_expand = true} (Context.Theory thy) (consts_of thy) thy;
+  certify_flags {prop = false, normalize = 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;
+  #1 o certify_flags {prop = false, normalize = false} (Context.Theory thy) (consts_of thy) thy;
 
 val cert_term = #1 oo certify_term;
 
 fun cert_prop thy =
-  #1 o certify_flags {prop = true, do_expand = true} (Context.Theory thy) (consts_of thy) thy;
+  #1 o certify_flags {prop = true, normalize = true} (Context.Theory thy) (consts_of thy) thy;
 
 end;