# HG changeset patch
# User wenzelm
# Date 1408442711 -7200
# Node ID 0ed1e999a0fb543291ba347a5a69d264123faf8f
# Parent  934d85f14d1db25903699a231a465691d60a5405
simplified type Proof.method;

diff -r 934d85f14d1d -r 0ed1e999a0fb src/HOL/Fun_Def.thy
--- 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 {*
diff -r 934d85f14d1d -r 0ed1e999a0fb src/HOL/Nominal/nominal_induct.ML
--- 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;
 
diff -r 934d85f14d1d -r 0ed1e999a0fb src/HOL/Nominal/nominal_primrec.ML
--- 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;
 
diff -r 934d85f14d1d -r 0ed1e999a0fb src/HOL/Tools/coinduction.ML
--- 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;
diff -r 934d85f14d1d -r 0ed1e999a0fb src/Pure/Isar/element.ML
--- 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
diff -r 934d85f14d1d -r 0ed1e999a0fb src/Pure/Isar/method.ML
--- 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;
diff -r 934d85f14d1d -r 0ed1e999a0fb src/Pure/Isar/proof.ML
--- 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
diff -r 934d85f14d1d -r 0ed1e999a0fb src/Tools/induct.ML
--- 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;