Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
insert: ignore facts;
authorwenzelm
Thu, 30 Sep 1999 21:21:04 +0200
changeset 7664 c151ac595551
parent 7663 460fedf14b09
child 7665 1ab0c74cd748
insert: ignore facts;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions 
--- 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