# HG changeset patch
# User wenzelm
# Date 1427474768 -3600
# Node ID 442b09c0f898f302eb3125a8fe18d57c865b3ea6
# Parent  9fb7661651ad75091bc812b7b11e124b0b2de0a7
tuned signature;

diff -r 9fb7661651ad -r 442b09c0f898 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Fri Mar 27 17:46:08 2015 +0100
@@ -176,7 +176,7 @@
           val tacs1 = [
             quant_tac ctxt 1,
             simp_tac (put_simpset HOL_ss ctxt) 1,
-            Induct_Tacs.induct_tac ctxt [[SOME "n"]] 1,
+            Induct_Tacs.induct_tac ctxt [[SOME "n"]] NONE 1,
             simp_tac (put_simpset take_ss ctxt addsimps prems) 1,
             TRY (safe_tac (put_claset HOL_cs ctxt))]
           fun con_tac _ = 
diff -r 9fb7661651ad -r 442b09c0f898 src/HOL/MicroJava/J/JTypeSafe.thy
--- a/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Fri Mar 27 17:46:08 2015 +0100
@@ -244,7 +244,7 @@
        THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*})
 
 -- "for if"
-apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] THEN_ALL_NEW
+apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW
   (asm_full_simp_tac @{context})) 7*})
 
 apply (tactic "forward_hyp_tac @{context}")
diff -r 9fb7661651ad -r 442b09c0f898 src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Mar 27 17:46:08 2015 +0100
@@ -131,7 +131,7 @@
                   (HOLogic.mk_exists ("x",@{typ nat},HOLogic.mk_eq (y,Const (ak_sign,inj_type) $ Bound 0)))
 
               val proof2 = fn {prems, context = ctxt} =>
-                Induct_Tacs.case_tac ctxt "y" [] 1 THEN
+                Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN
                 asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN
                 rtac @{thm exI} 1 THEN
                 rtac @{thm refl} 1
diff -r 9fb7661651ad -r 442b09c0f898 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Mar 27 11:38:26 2015 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Mar 27 17:46:08 2015 +0100
@@ -798,7 +798,7 @@
 fun split_idle_tac ctxt =
   SELECT_GOAL
    (TRY (rtac @{thm actionI} 1) THEN
-    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] 1 THEN
+    Induct_Tacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN
     rewrite_goals_tac ctxt @{thms action_rews} THEN
     forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
     asm_full_simp_tac ctxt 1);
diff -r 9fb7661651ad -r 442b09c0f898 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Fri Mar 27 11:38:26 2015 +0100
+++ b/src/Tools/induct_tacs.ML	Fri Mar 27 17:46:08 2015 +0100
@@ -7,11 +7,9 @@
 signature INDUCT_TACS =
 sig
   val case_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
-    int -> tactic
-  val case_rule_tac: Proof.context -> string -> (binding * string option * mixfix) list ->
-    thm -> int -> tactic
-  val induct_tac: Proof.context -> string option list list -> int -> tactic
-  val induct_rules_tac: Proof.context -> string option list list -> thm list -> int -> tactic
+    thm option -> int -> tactic
+  val induct_tac: Proof.context -> string option list list ->
+    thm list option -> int -> tactic
 end
 
 structure Induct_Tacs: INDUCT_TACS =
@@ -28,7 +26,7 @@
         quote (Syntax.string_of_term ctxt u) ^ Position.here pos);
   in (u, U) end;
 
-fun gen_case_tac ctxt s fixes opt_rule i st =
+fun case_tac ctxt s fixes opt_rule i st =
   let
     val rule =
       (case opt_rule of
@@ -55,9 +53,6 @@
   in Rule_Insts.res_inst_tac ctxt [((xi, Position.none), s)] fixes rule i st end
   handle THM _ => Seq.empty;
 
-fun case_tac ctxt s xs = gen_case_tac ctxt s xs NONE;
-fun case_rule_tac ctxt s xs rule = gen_case_tac ctxt s xs (SOME rule);
-
 
 (* induction *)
 
@@ -72,7 +67,7 @@
 
 in
 
-fun gen_induct_tac ctxt0 varss opt_rules i st =
+fun induct_tac ctxt0 varss opt_rules i st =
   let
     val ((_, goal), ctxt) = Variable.focus_subgoal i st ctxt0;
     val (prems, concl) = Logic.strip_horn (Thm.term_of goal);
@@ -117,9 +112,6 @@
 
 end;
 
-fun induct_tac ctxt args = gen_induct_tac ctxt args NONE;
-fun induct_rules_tac ctxt args rules = gen_induct_tac ctxt args (SOME rules);
-
 
 (* method syntax *)
 
@@ -139,14 +131,13 @@
   Theory.setup
    (Method.setup @{binding case_tac}
       (Args.goal_spec -- Scan.lift (Args.name_inner_syntax -- Parse.for_fixes) -- opt_rule >>
-        (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (gen_case_tac ctxt s xs r)))
+        (fn ((quant, (s, xs)), r) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s xs r)))
       "unstructured case analysis on types" #>
     Method.setup @{binding induct_tac}
       (Args.goal_spec -- varss -- opt_rules >>
-        (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (gen_induct_tac ctxt vs rs)))
+        (fn ((quant, vs), rs) => fn ctxt => SIMPLE_METHOD'' quant (induct_tac ctxt vs rs)))
       "unstructured induction on types");
 
 end;
 
 end;
-