aboutsummaryrefslogtreecommitdiff
path: root/spartan/core
diff options
context:
space:
mode:
Diffstat (limited to 'spartan/core')
-rw-r--r--spartan/core/Spartan.thy3
-rw-r--r--spartan/core/context_tactical.ML2
2 files changed, 3 insertions, 2 deletions
diff --git a/spartan/core/Spartan.thy b/spartan/core/Spartan.thy
index ea72208..7f13036 100644
--- a/spartan/core/Spartan.thy
+++ b/spartan/core/Spartan.thy
@@ -248,7 +248,8 @@ method_setup intros =
K (CONTEXT_METHOD (fn facts =>
case n_opt of
SOME n => CREPEAT_N n (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))
- | NONE => CREPEAT (CCHANGED (CHEADGOAL (SIDE_CONDS 0 intro_ctac facts))))))\<close>
+ | NONE => CCHANGED (CREPEAT (CCHANGED (
+ CHEADGOAL (SIDE_CONDS 0 intro_ctac facts)))))))\<close>
method_setup elim =
\<open>Scan.repeat Args.term >> (fn tms => K (CONTEXT_METHOD (
diff --git a/spartan/core/context_tactical.ML b/spartan/core/context_tactical.ML
index 0aa6f20..d0fed61 100644
--- a/spartan/core/context_tactical.ML
+++ b/spartan/core/context_tactical.ML
@@ -92,7 +92,7 @@ fun CREPEAT ctac =
fun CREPEAT1 ctac = ctac CTHEN CREPEAT ctac
-fun CREPEAT_N 0 _ = all_ctac
+fun CREPEAT_N 0 _ = no_ctac
| CREPEAT_N n ctac = ctac CTHEN CREPEAT_N (n - 1) ctac
fun CFILTER pred ctac cst =