diff -r 9067932c2182 -r 2301ec62fdca src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Oct 14 11:13:26 2024 +0200 +++ b/src/Pure/Syntax/syntax.ML Mon Oct 14 11:16:11 2024 +0200 @@ -482,9 +482,8 @@ "Cycle in syntax consts: " ^ (space_implode " \ " (map quote cs))) css)); fun get_consts (Syntax ({consts, ...}, _)) c = - if Graph.defined consts c then - Graph.all_preds consts [c] - |> filter (Graph.Keys.is_empty o Graph.imm_preds consts) + if Graph.defined consts c + then filter (Graph.is_minimal consts) (Graph.all_preds consts [c]) else [c]; fun update_consts (c, bs) consts =