# HG changeset patch
# User berghofe
# Date 939820695 -7200
# Node ID 5a3fa0c4b21521bb87d4d389a7c9c7b78682a87f
# Parent  adf6b1112bc153b7b243298fdb8570402cb83fb0
Eliminated mutual_induct_tac.

diff -r adf6b1112bc1 -r 5a3fa0c4b215 NEWS
--- a/NEWS	Wed Oct 13 15:16:52 1999 +0200
+++ b/NEWS	Wed Oct 13 15:18:15 1999 +0200
@@ -17,6 +17,9 @@
 
 * HOL: the predicate "inj" is now defined by translation to "inj_on";
 
+* HOL/datatype: mutual_induct_tac no longer exists --
+  use induct_tac "x_1 ... x_n" instead of mutual_induct_tac ["x_1", ..., "x_n"]
+
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;
 
diff -r adf6b1112bc1 -r 5a3fa0c4b215 src/HOL/Induct/ABexp.ML
--- a/src/HOL/Induct/ABexp.ML	Wed Oct 13 15:16:52 1999 +0200
+++ b/src/HOL/Induct/ABexp.ML	Wed Oct 13 15:18:15 1999 +0200
@@ -12,7 +12,7 @@
 Goal
   "evala env (substa (Var(v := a')) a) = evala (env(v := evala env a')) a &  \
  \ evalb env (substb (Var(v := a')) b) = evalb (env(v := evala env a')) b";
-by (mutual_induct_tac ["a","b"] 1);
+by (induct_tac "a b" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst1_aexp_bexp";
 
@@ -20,6 +20,6 @@
 Goal
   "evala env (substa s a) = evala (%x. evala env (s x)) a &  \
  \ evalb env (substb s b) = evalb (%x. evala env (s x)) b";
-by (mutual_induct_tac ["a","b"] 1);
+by (induct_tac "a b" 1);
 by (Auto_tac);
 qed "subst_all_aexp_bexp";
diff -r adf6b1112bc1 -r 5a3fa0c4b215 src/HOL/Induct/Term.ML
--- a/src/HOL/Induct/Term.ML	Wed Oct 13 15:16:52 1999 +0200
+++ b/src/HOL/Induct/Term.ML	Wed Oct 13 15:18:15 1999 +0200
@@ -12,7 +12,7 @@
   \  (subst_term f1 (subst_term f2 t)) &  \
   \  (subst_term_list ((subst_term f1) o f2) ts) =  \
   \  (subst_term_list f1 (subst_term_list f2 ts))";
-by (mutual_induct_tac ["t", "ts"] 1);
+by (induct_tac "t ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_comp";
 
@@ -23,7 +23,7 @@
    \  !!f ts. list_all P ts ==> P (App f ts) |] ==>  \
    \    P t & list_all P ts"
   (fn prems =>
-    [mutual_induct_tac ["t", "ts"] 1,
+    [induct_tac "t ts" 1,
      resolve_tac prems 1,
      resolve_tac prems 1,
      atac 1,
diff -r adf6b1112bc1 -r 5a3fa0c4b215 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Oct 13 15:16:52 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Wed Oct 13 15:18:15 1999 +0200
@@ -8,7 +8,6 @@
 
 signature BASIC_DATATYPE_PACKAGE =
 sig
-  val mutual_induct_tac : string list -> int -> tactic
   val induct_tac : string -> int -> tactic
   val exhaust_tac : string -> int -> tactic
   val distinct_simproc : simproc
@@ -170,8 +169,9 @@
 
 (* generic induction tactic for datatypes *)
 
-fun mutual_induct_tac vars i state =
+fun induct_tac s i state =
   let
+    val vars = Syntax.read_idents s;
     val (_, _, Bi, _) = dest_state (state, i);
     val {sign, ...} = rep_thm state;
     val tn = find_tname (hd vars) Bi;
@@ -185,8 +185,6 @@
     occs_in_prems (res_inst_tac insts induction) vars i state
   end;
 
-fun induct_tac var = mutual_induct_tac [var];
-
 (* generic exhaustion tactic for datatypes *)
 
 fun exhaust_tac aterm i state =