# HG changeset patch
# User wenzelm
# Date 1213478402 -7200
# Node ID 6724f31a1c8e06a51ebfe26eb6c5194bf915c349
# Parent  2a8d03e0bbb97b6bc45927f5980a8ff664e5a3fc
removed unused excluded_middle_tac;
proper context for tactics derived from res_inst_tac;
tuned setup;

diff -r 2a8d03e0bbb9 -r 6724f31a1c8e src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sat Jun 14 23:20:00 2008 +0200
+++ b/src/FOL/FOL.thy	Sat Jun 14 23:20:02 2008 +0200
@@ -60,12 +60,6 @@
   apply assumption
   done
 
-(*For disjunctive case analysis*)
-ML {*
-  fun excluded_middle_tac sP =
-    res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
-*}
-
 lemma case_split [case_names True False]:
   assumes r1: "P ==> Q"
     and r2: "~P ==> Q"
@@ -76,9 +70,14 @@
   done
 
 ML {*
-  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split}
+  fun case_tac ctxt a =
+    RuleInsts.res_inst_tac ctxt [(("P", 0), a)] @{thm case_split}
 *}
 
+method_setup case_tac =
+  {* Method.goal_args_ctxt Args.name case_tac *}
+  "case_tac emulation (dynamic instantiation!)"
+
 
 (*** Special elimination rules *)
 
@@ -169,7 +168,6 @@
 use "cladata.ML"
 setup Cla.setup
 setup cla_setup
-setup case_setup
 
 use "blastdata.ML"
 setup Blast.setup
diff -r 2a8d03e0bbb9 -r 6724f31a1c8e src/FOL/cladata.ML
--- a/src/FOL/cladata.ML	Sat Jun 14 23:20:00 2008 +0200
+++ b/src/FOL/cladata.ML	Sat Jun 14 23:20:02 2008 +0200
@@ -37,8 +37,3 @@
                      addSEs [@{thm exE}, @{thm alt_ex1E}] addEs [@{thm allE}];
 
 val cla_setup = Cla.map_claset (K FOL_cs);
-
-val case_setup =
- (Method.add_methods
-    [("case_tac", Method.goal_args Args.name case_tac,
-      "case_tac emulation (dynamic instantiation!)")]);