# HG changeset patch
# User wenzelm
# Date 1400683574 -7200
# Node ID d2fb95869d55f01fa0b2345dd02ba4fda1b81992
# Parent  aceaca232177a66b1fa370eb8134bed0d8cfa9a5# Parent  042d6e58cb404fffde93e0b20d5e946fe0165dcb
merged

diff -r 042d6e58cb40 -r d2fb95869d55 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Wed May 21 16:21:11 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Wed May 21 16:46:14 2014 +0200
@@ -115,11 +115,8 @@
        breakpoints = breakpoints})
   in Thm.declaration_attribute (K update) end
 
-fun term_breakpoint terms =
-  Thm.declaration_attribute (K (fold add_term_breakpoint terms))
-
-val thm_breakpoint =
-  Thm.declaration_attribute add_thm_breakpoint
+fun breakpoint terms =
+  Thm.declaration_attribute (fn thm => add_thm_breakpoint thm o fold add_term_breakpoint terms)
 
 
 
@@ -419,12 +416,9 @@
     (fn (((interactive, mode), depth), memory) => config mode interactive depth memory)
 
 val _ = Theory.setup
-  (Attrib.setup @{binding break_term}
-    (Scan.repeat1 Args.term_pattern >> term_breakpoint)
-    "declaration of a term breakpoint" #>
-   Attrib.setup @{binding break_thm}
-    (Scan.succeed thm_breakpoint)
-    "declaration of a theorem breakpoint" #>
+  (Attrib.setup @{binding simp_break}
+    (Scan.repeat Args.term_pattern >> breakpoint)
+    "declaration of a simplifier breakpoint" #>
    Attrib.setup @{binding simplifier_trace} (Scan.lift config_parser)
     "simplifier trace configuration")