# HG changeset patch
# User wenzelm
# Date 1728897371 -7200
# Node ID 2301ec62fdca3066715ddf9483b07a761132afe2
# Parent  9067932c2182ae6a4b45ab1bdffc3e647c6872ec
tuned;

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 " \<leadsto> " (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 =