--- a/src/HOL/Fun_Def.thy Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Fun_Def.thy Tue Aug 19 12:05:11 2014 +0200
@@ -103,7 +103,7 @@
ML_file "Tools/Function/induction_schema.ML"
method_setup induction_schema = {*
- Scan.succeed (RAW_METHOD o Induction_Schema.induction_schema_tac)
+ Scan.succeed (NO_CASES oo Induction_Schema.induction_schema_tac)
*} "prove an induction principle"
setup {*
--- a/src/HOL/Nominal/nominal_induct.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Aug 19 12:05:11 2014 +0200
@@ -172,9 +172,8 @@
Scan.lift (Args.mode Induct.no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
- (fn (no_simp, (((x, y), z), w)) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts)));
+ (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
+ HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
end;
--- a/src/HOL/Nominal/nominal_primrec.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Tue Aug 19 12:05:11 2014 +0200
@@ -373,9 +373,10 @@
|> snd
end)
[goals] |>
- Proof.apply (Method.Basic (fn ctxt => RAW_METHOD (fn _ =>
- rewrite_goals_tac ctxt defs_thms THEN
- compose_tac (false, rule, length rule_prems) 1))) |>
+ Proof.apply (Method.Basic (fn ctxt => fn _ =>
+ NO_CASES
+ (rewrite_goals_tac ctxt defs_thms THEN
+ compose_tac (false, rule, length rule_prems) 1))) |>
Seq.hd
end;
--- a/src/HOL/Tools/coinduction.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/HOL/Tools/coinduction.ML Tue Aug 19 12:05:11 2014 +0200
@@ -149,9 +149,8 @@
val setup =
Method.setup @{binding coinduction}
(arbitrary -- Scan.option coinduct_rule >>
- (fn (arbitrary, opt_rule) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts))))
+ (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
+ Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
"coinduction on types or predicates/sets";
end;
--- a/src/Pure/Isar/element.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/Pure/Isar/element.ML Tue Aug 19 12:05:11 2014 +0200
@@ -270,8 +270,8 @@
local
val refine_witness =
- Proof.refine (Method.Basic (K (RAW_METHOD
- (K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI))))))))));
+ Proof.refine (Method.Basic (K (NO_CASES o
+ K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (rtac Drule.protectI)))))))));
fun gen_witness_proof proof after_qed wit_propss eq_props =
let
--- a/src/Pure/Isar/method.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/Pure/Isar/method.ML Tue Aug 19 12:05:11 2014 +0200
@@ -6,10 +6,7 @@
signature METHOD =
sig
- type method
- val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
- val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
- val RAW_METHOD: (thm list -> tactic) -> method
+ type method = thm list -> cases_tactic
val METHOD_CASES: (thm list -> cases_tactic) -> method
val METHOD: (thm list -> tactic) -> method
val fail: method
@@ -90,18 +87,10 @@
(* datatype method *)
-datatype method = Meth of thm list -> cases_tactic;
-
-fun apply meth ctxt = let val Meth m = meth ctxt in m end;
-
-val RAW_METHOD_CASES = Meth;
+type method = thm list -> cases_tactic;
-fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
-
-fun METHOD_CASES tac = RAW_METHOD_CASES (fn facts =>
- Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts));
-
-fun METHOD tac = RAW_METHOD (fn facts => ALLGOALS Goal.conjunction_tac THEN tac facts);
+fun METHOD_CASES tac facts = Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
+fun METHOD tac facts = NO_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
val fail = METHOD (K no_tac);
val succeed = METHOD (K all_tac);
@@ -154,7 +143,7 @@
fun atomize false ctxt =
SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
| atomize true ctxt =
- RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt)));
+ NO_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
(* this -- resolve facts directly *)
@@ -277,7 +266,7 @@
in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
fun tactic source ctxt = METHOD (ml_tactic source ctxt);
-fun raw_tactic source ctxt = RAW_METHOD (ml_tactic source ctxt);
+fun raw_tactic source ctxt = NO_CASES o ml_tactic source ctxt;
@@ -376,7 +365,7 @@
val (src1, meth) = check_src ctxt0 src0;
val src2 = Args.init_assignable src1;
val ctxt = Context_Position.not_really ctxt0;
- val _ = Seq.pull (apply (method ctxt src2) ctxt [] (Goal.protect 0 Drule.dummy_thm));
+ val _ = Seq.pull (method ctxt src2 ctxt [] (Goal.protect 0 Drule.dummy_thm));
in Args.closure src2 end;
fun method_cmd ctxt = method ctxt o method_closure ctxt;
@@ -553,8 +542,6 @@
end;
-val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
-val RAW_METHOD = Method.RAW_METHOD;
val METHOD_CASES = Method.METHOD_CASES;
val METHOD = Method.METHOD;
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
--- a/src/Pure/Isar/proof.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/Pure/Isar/proof.ML Tue Aug 19 12:05:11 2014 +0200
@@ -401,7 +401,7 @@
find_goal state;
val ctxt = if current_context then context_of state else goal_ctxt;
in
- Method.apply method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
+ method ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
state
|> map_goal
(Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #>
@@ -892,9 +892,9 @@
in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
- refine (Method.Basic (K (RAW_METHOD
- (K (HEADGOAL (PRECISE_CONJUNCTS n
- (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
+ refine (Method.Basic (K (NO_CASES o
+ K (HEADGOAL (PRECISE_CONJUNCTS n
+ (HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))
#> Seq.hd;
in
--- a/src/Tools/induct.ML Mon Aug 18 15:46:27 2014 +0200
+++ b/src/Tools/induct.ML Tue Aug 19 12:05:11 2014 +0200
@@ -932,15 +932,13 @@
(cases_tac ctxt (not no_simp) insts opt_rule facts)))))
"case analysis on types or predicates/sets";
-fun gen_induct_setup binding itac =
+fun gen_induct_setup binding tac =
Method.setup binding
(Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
- (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM
- (HEADGOAL (itac ctxt (not no_simp) insts arbitrary taking opt_rule facts)))))
+ (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
+ Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
"induction on types or predicates/sets";
val induct_setup = gen_induct_setup @{binding induct} induct_tac;
@@ -948,9 +946,8 @@
val coinduct_setup =
Method.setup @{binding coinduct}
(Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
- (fn ((insts, taking), opt_rule) => fn ctxt =>
- RAW_METHOD_CASES (fn facts =>
- Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts)))))
+ (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
+ Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
"coinduction on types or predicates/sets";
end;