Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/method.ML
changeset 7664 c151ac595551
parent 7611 5b5aba10c8f6
child 8093 d5eb246c94ec 
--- 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"),
isabelle