proper term equality;
proper Args.term_pattern parser (like 'is' or 'let' in Isar);

--- a/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 20:32:58 2014 +0100
+++ b/src/Pure/Tools/simplifier_trace.ML	Tue Feb 18 20:37:45 2014 +0100
@@ -23,7 +23,7 @@
   | merge_modes Full _ = Full
 
 val empty_breakpoints =
-  (Item_Net.init (op =) single (* FIXME equality on terms? *),
+  (Item_Net.init (op aconv) single,
    Item_Net.init eq_rrule (single o Thm.full_prop_of o #thm))
 
 fun merge_breakpoints ((term_bs1, thm_bs1), (term_bs2, thm_bs2)) =
@@ -411,18 +411,15 @@
 
 (** attributes **)
 
-val pat_parser =
-  Args.context -- Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_schematic
-
-val mode_parser: string parser =
+val mode_parser =
   Scan.optional
     (Args.$$$ "mode" |-- Args.$$$ "=" |-- (Args.$$$ "normal" || Args.$$$ "full"))
     "normal"
 
-val interactive_parser: bool parser =
+val interactive_parser =
   Scan.optional (Args.$$$ "interactive" >> K true) false
 
-val memory_parser: bool parser =
+val memory_parser =
   Scan.optional (Args.$$$ "no_memory" >> K false) true
 
 val depth_parser =
@@ -434,7 +431,7 @@
 
 val _ = Theory.setup
   (Attrib.setup @{binding break_term}
-    ((Scan.repeat1 pat_parser) >> term_breakpoint)
+    (Scan.repeat1 Args.term_pattern >> term_breakpoint)
     "declaration of a term breakpoint" #>
    Attrib.setup @{binding break_thm}
     (Scan.succeed thm_breakpoint)