# HG changeset patch # User wenzelm # Date 1704839934 -3600 # Node ID f0fab78a418a4a5f9cfb12a52426041ad3287f3e # Parent d7f32f04bd1343549ee5d82b42f336a4129e7d2b tuned; diff -r d7f32f04bd13 -r f0fab78a418a src/Pure/consts.ML --- a/src/Pure/consts.ML Tue Jan 09 22:40:38 2024 +0100 +++ b/src/Pure/consts.ML Tue Jan 09 23:38:54 2024 +0100 @@ -169,25 +169,27 @@ fun err msg (c, T) = raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Syntax.string_of_typ (Syntax.init_pretty context) T, [], []); - val certT = Type.certify_typ Type.mode_default tsig; - fun cert tm = + + fun err_const const = err "Illegal type for constant" const; + + val expand_typ = Type.certify_typ Type.mode_default tsig; + fun expand_term tm = let val (head, args) = Term.strip_comb tm; - val args' = map cert args; + val args' = map expand_term args; fun comb head' = Term.list_comb (head', args'); in (case head of - Abs (x, T, t) => comb (Abs (x, certT T, cert t)) + Abs (x, T, t) => comb (Abs (x, expand_typ T, expand_term t)) | Const (c, T) => let - val T' = certT T; + val T' = expand_typ T; val (_, ({T = U, ...}, abbr)) = the_entry consts c; fun expand u = Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ => err "Illegal type for abbreviation" (c, T), args'); in - if not (Type.raw_instance (T', U)) then - err "Illegal type for constant" (c, T) + if not (Type.raw_instance (T', U)) then err_const (c, T) else (case abbr of SOME {rhs, normal_rhs, force_expand} => @@ -198,7 +200,7 @@ end | _ => comb head) end; - in cert end; + in expand_term end; (* typargs -- view actual const type as instance of declaration *)