diff -r 57bfacbbaeda -r 528f7489a403 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Mon Sep 30 16:34:56 2002 +0200
+++ b/src/Provers/simplifier.ML	Mon Sep 30 16:36:57 2002 +0200
@@ -475,6 +475,7 @@
 val no_asmN = "no_asm";
 val no_asm_useN = "no_asm_use";
 val no_asm_simpN = "no_asm_simp";
+val asm_lrN = "asm_lr";
 
 val simp_attr =
  (Attrib.add_del_args simp_add_global simp_del_global,
@@ -525,6 +526,7 @@
  (Args.parens (Args.$$$ no_asmN) >> K simp_tac ||
   Args.parens (Args.$$$ no_asm_simpN) >> K asm_simp_tac ||
   Args.parens (Args.$$$ no_asm_useN) >> K full_simp_tac ||
+  Args.parens (Args.$$$ asm_lrN) >> K asm_lr_simp_tac ||
   Scan.succeed asm_full_simp_tac);
 
 val cong_modifiers =