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.
COMP_INCR;
authorwenzelm
Wed, 29 Nov 2006 04:11:12 +0100
changeset 21579 abd2b4386a63
parent 21578 a89f786b301a
child 21580 ff8062cd41e9
COMP_INCR;
src/Pure/Isar/method.ML file | annotate | diff | comparison | revisions
src/Pure/goal.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/method.ML	Wed Nov 29 04:11:11 2006 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 29 04:11:12 2006 +0100
@@ -151,11 +151,8 @@
 
 local
 
-fun cut_rule_tac raw_rule =
-  let
-    val rule = Drule.forall_intr_vars raw_rule;
-    val revcut_rl = Drule.incr_indexes rule Drule.revcut_rl;
-  in Tactic.rtac (rule COMP revcut_rl) end;
+fun cut_rule_tac rule =
+  Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
 
 in
 
--- a/src/Pure/goal.ML	Wed Nov 29 04:11:11 2006 +0100
+++ b/src/Pure/goal.ML	Wed Nov 29 04:11:12 2006 +0100
@@ -48,7 +48,7 @@
   --- (protect)
   #C
 *)
-fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
+fun protect th = th COMP_INCR Drule.protectI;
 
 (*
   A ==> ... ==> #C
isabelle