# HG changeset patch
# User wenzelm
# Date 938719264 -7200
# Node ID c151ac5955516966aaa9e9a595addd44ea216004
# Parent  460fedf14b09006f3a2df0d8cd03af47c19382c8
insert: ignore facts;

diff -r 460fedf14b09 -r c151ac595551 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Thu Sep 30 21:20:36 1999 +0200
+++ b/src/Pure/Isar/method.ML	Thu Sep 30 21:21:04 1999 +0200
@@ -112,7 +112,7 @@
   | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
 
 val insert_facts = METHOD (ALLGOALS o insert_tac);
-fun insert thms = METHOD (fn facts => ALLGOALS (insert_tac (thms @ facts)));
+fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
 
 end;
 
@@ -384,7 +384,7 @@
  [("fail", no_args fail, "force failure"),
   ("succeed", no_args succeed, "succeed"),
   ("-", no_args insert_facts, "do nothing, inserting current facts only"),
-  ("insert", thms_args insert, "insert facts (improper!)"),
+  ("insert", thms_args insert, "insert theorems, ignoring facts (improper!)"),
   ("unfold", thms_args unfold, "unfold definitions"),
   ("fold", thms_args fold, "fold definitions"),
   ("rule", thms_args rule, "apply some rule"),