src/Pure/Tools/simplifier_trace.ML
changeset 80712 05b16602a683
parent 80306 c2537860ccf8
--- a/src/Pure/Tools/simplifier_trace.ML	Thu Aug 15 12:22:39 2024 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Thu Aug 15 12:43:17 2024 +0200
@@ -87,7 +87,7 @@
 
 fun add_thm_breakpoint thm context =
   let
-    val rrules = mk_rrules (Context.proof_of context) [thm]
+    val rrules = mk_rrules (Context.proof_of context) thm
   in
     map_breakpoints (apsnd (fold Item_Net.update rrules)) context
   end