author | wenzelm |
Wed, 10 Jan 2024 13:24:59 +0100 | |
changeset 79467 | aeb775b438c6 |
parent 79466 | ec3dc36551ab |
child 79468 | 953ada87ea37 |
--- a/src/Pure/consts.ML Wed Jan 10 13:18:28 2024 +0100 +++ b/src/Pure/consts.ML Wed Jan 10 13:24:59 2024 +0100 @@ -179,8 +179,8 @@ val need_expand = Term.exists_Const (fn (c, _) => - (case the_entry consts c of - (_, SOME {force_expand, ...}) => do_expand orelse force_expand + (case get_entry consts c of + SOME (_, SOME {force_expand, ...}) => do_expand orelse force_expand | _ => false)); val expand_typ = Type.certify_typ Type.mode_default tsig;