src/Pure/Isar/context_rules.ML
changeset 82848 0a8977dcb21a
parent 82847 d8ecaff223ff
child 82850 3020b1660bec
--- a/src/Pure/Isar/context_rules.ML	Fri Jul 11 15:17:42 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Jul 11 21:36:22 2025 +0200
@@ -49,8 +49,8 @@
 fun insert_decl ({kind, tag, info = th}: decl) =
   Bires.insert_tagged_rule (tag, Bires.kind_rule kind th);
 
-fun remove_decl ({info = th, ...}: decl) =
-  Bires.delete_tagged_rule (false, th) o Bires.delete_tagged_rule (true, th);
+fun remove_decl ({tag = {index, ...}, info = th, ...}: decl) =
+  Bires.delete_tagged_rule (index, th);
 
 
 (* context data *)