# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1400682364 -7200
# Node ID aceaca232177a66b1fa370eb8134bed0d8cfa9a5
# Parent  fc96f394c7e58a3ce551f09f29b0d601df84b762
consolidate "break_thm" and "break_term" attributes into "simp_break";

diff -r fc96f394c7e5 -r aceaca232177 src/Pure/Tools/simplifier_trace.ML
--- a/src/Pure/Tools/simplifier_trace.ML	Wed May 21 14:09:43 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.ML	Wed May 21 16:26:04 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")