# HG changeset patch
# User wenzelm
# Date 936213758 -7200
# Node ID 28b48fcb0d55829d38417a67cddf5ade82a9c48d
# Parent  c63d619286a3b144eec228fc5726a448b280460f
Method.insert_tac;
tuned comments;

diff -r c63d619286a3 -r 28b48fcb0d55 src/Provers/simplifier.ML
--- a/src/Provers/simplifier.ML	Wed Sep 01 21:21:22 1999 +0200
+++ b/src/Provers/simplifier.ML	Wed Sep 01 21:22:38 1999 +0200
@@ -473,7 +473,7 @@
 fun simp_meth thin cut tac ctxt = Method.METHOD (fn facts =>
   FIRSTGOAL
     ((if thin then REPEAT_DETERM o etac Drule.thin_rl else K all_tac)
-      THEN' (if cut then Method.same_tac facts else K all_tac)
+      THEN' (if cut then Method.insert_tac facts else K all_tac)
       THEN' tac (get_local_simpset ctxt)));
 
 val simp_method = simp_args ooo simp_meth;
@@ -482,9 +482,10 @@
 (* setup_methods *)
 
 val setup_methods = Method.add_methods
- [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac), "simplification"),
+ [(simpN,               simp_method true true (CHANGED oo asm_full_simp_tac),
+    "full simplification (including facts, excluding assumptions)"),
   (asm_simpN,           simp_method false true (CHANGED oo asm_full_simp_tac),
-    "simplification (including assumption)"),
+    "full simplification (including facts and assumptions)"),
   ("simp_tac",          simp_method false false simp_tac, "simp_tac (improper!)"),
   ("asm_simp_tac",      simp_method false false asm_simp_tac, "asm_simp_tac (improper!)"),
   ("full_simp_tac",     simp_method false false full_simp_tac, "full_simp_tac (improper!)"),