# HG changeset patch
# User berghofe
# Date 901279178 -7200
# Node ID 9b8547a9496afa9c74bd507626d698437c36684e
# Parent  89f162de39cf44c7dacef48b49b8aa84a85c2c69
Adapted to new datatype package.

diff -r 89f162de39cf -r 9b8547a9496a src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -83,10 +83,10 @@
   by (rename_tac "ex1 ex2 n" 1);
   by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
   by (Asm_full_simp_tac 1);
-  by (nat_ind_tac "n" 1);
+  by (induct_tac "n" 1);
    by (fast_tac (claset() addIs [p1,reachable_0]) 1);
-  by (eres_inst_tac[("x","n")] allE 1);
-  by (exhaust_tac "ex1 n" 1 THEN ALLGOALS Asm_full_simp_tac);
+  by (eres_inst_tac[("x","na")] allE 1);
+  by (exhaust_tac "ex1 na" 1 THEN ALLGOALS Asm_full_simp_tac);
   by Safe_tac;
    by (etac (p2 RS mp) 1);
     by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -79,7 +79,7 @@
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [split_option_case]) 1);
+                addsplits [option.split]) 1);
 qed"comp1_reachable";
 
 
@@ -99,7 +99,7 @@
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [split_option_case]) 1);
+                addsplits [option.split]) 1);
 qed"comp2_reachable";
 
 Delsplits [split_if];
@@ -161,7 +161,7 @@
 by (asm_full_simp_tac
       (simpset() addsimps [executions_def,is_execution_fragment_def,
                           par_def,starts_of_def,trans_of_def,rename_def]
-                addsplits [split_option_case]) 1);
+                addsplits [option.split]) 1);
 by (best_tac (claset() addSDs [spec] addDs [sym] addss (simpset())) 1);
 qed"reachable_rename_ioa";
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/Com.thy
--- a/src/HOL/Induct/Com.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Com.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -6,7 +6,7 @@
 Example of Mutual Induction via Iteratived Inductive Definitions: Commands
 *)
 
-Com = Arith + Inductive +
+Com = Datatype +
 
 types loc
       state = "loc => nat"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/Comb.thy
--- a/src/HOL/Induct/Comb.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Comb.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -13,7 +13,7 @@
 *)
 
 
-Comb = Arith + Inductive +
+Comb = Datatype +
 
 (** Datatype definition of combinators S and K, with infixed application **)
 datatype comb = K
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/LList.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -155,10 +155,10 @@
 by (safe_tac ((claset_of Fun.thy) delrules [equalityI]));
 by (etac LListD.elim 1);
 by (safe_tac (claset_of Prod.thy delrules [equalityI] addSEs [diagE]));
-by (res_inst_tac [("n", "n")] natE 1);
+by (exhaust_tac "n" 1);
 by (Asm_simp_tac 1);
 by (rename_tac "n'" 1);
-by (res_inst_tac [("n", "n'")] natE 1);
+by (exhaust_tac "n'" 1);
 by (asm_simp_tac (simpset() addsimps [CONS_def]) 1);
 by (asm_simp_tac (simpset() addsimps [CONS_def, less_Suc_eq]) 1);
 qed "LListD_implies_ntrunc_equality";
@@ -317,9 +317,9 @@
 by (stac prem2 1);
 by (Simp_tac 1);
 by (strip_tac 1);
-by (res_inst_tac [("n", "n")] natE 1);
+by (exhaust_tac "n" 1);
 by (rename_tac "m" 2);
-by (res_inst_tac [("n", "m")] natE 2);
+by (exhaust_tac "m" 2);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [less_Suc_eq])));
 result();
 
@@ -782,12 +782,12 @@
 Goal
     "nat_rec (LCons b l) (%m. lmap(f)) n =      \
 \    LCons (nat_rec b (%m. f) n) (nat_rec l (%m. lmap(f)) n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "fun_power_lmap";
 
 goal Nat.thy "nat_rec (g x) (%m. g) n = nat_rec x (%m. g) (Suc n)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "fun_power_Suc";
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -44,7 +44,7 @@
 qed "Sigma_Suc2";
 
 Goal "{i} Times below(n+n) : tiling domino";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Un_assoc RS sym, Sigma_Suc2])));
 by (resolve_tac tiling.intrs 1);
 by (assume_tac 2);
@@ -57,7 +57,7 @@
 qed "dominoes_tile_row";
 
 Goal "(below m) Times below(n+n) : tiling domino";
-by (nat_ind_tac "m" 1);
+by (induct_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Sigma_Suc1])));
 by (blast_tac (claset() addSIs [tiling_UnI, dominoes_tile_row]
                        addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/Perm.ML
--- a/src/HOL/Induct/Perm.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/Perm.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -14,7 +14,7 @@
 open Perm;
 
 Goal "l <~~> l";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (REPEAT (ares_tac perm.intrs 1));
 qed "perm_refl";
 
@@ -50,7 +50,7 @@
 
 (*We can insert the head anywhere in the list*)
 Goal "a # xs @ ys <~~> xs @ a # ys";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (simp_tac (simpset() addsimps [perm_refl]) 1);
 by (Simp_tac 1);
 by (etac ([perm.swap, perm.Cons] MRS perm.trans) 1);
@@ -63,7 +63,7 @@
 *)
 
 Goal "xs@ys <~~> ys@xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (simp_tac (simpset() addsimps [perm_refl]) 1);
 by (Simp_tac 1);
 by (etac ([perm.Cons, perm_append_Cons] MRS perm.trans) 1);
@@ -77,7 +77,7 @@
 qed "perm_append_single";
 
 Goal "rev xs <~~> xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (simp_tac (simpset() addsimps [perm_refl]) 1);
 by (Simp_tac 1);
 by (rtac (perm_append_single RS perm_sym RS perm.trans) 1);
@@ -85,7 +85,7 @@
 qed "perm_rev";
 
 Goal "xs <~~> ys ==> l@xs <~~> l@ys";
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [perm.Cons]) 1);
 qed "perm_append1";
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/PropLog.ML
--- a/src/HOL/Induct/PropLog.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/PropLog.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -102,7 +102,7 @@
 (*This formulation is required for strong induction hypotheses*)
 Goal "hyps p tt |- (if tt[p] then p else p->false)";
 by (rtac (split_if RS iffD2) 1);
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [thms_I, thms.H])));
 by (fast_tac (claset() addIs [weaken_left_Un1, weaken_left_Un2, 
 			      weaken_right, imp_false]
@@ -140,7 +140,7 @@
 (*For the case hyps(p,t)-insert(#v,Y) |- p;
   we also have hyps(p,t)-{#v} <= hyps(p, t-{v}) *)
 Goal "hyps p (t-{v}) <= insert (#v->false) ((hyps p t)-{#v})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_Diff";
@@ -148,7 +148,7 @@
 (*For the case hyps(p,t)-insert(#v -> false,Y) |- p;
   we also have hyps(p,t)-{#v->false} <= hyps(p, insert(v,t)) *)
 Goal "hyps p (insert v t) <= insert (#v) (hyps p t-{#v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Fast_tac 1);
 qed "hyps_insert";
@@ -169,7 +169,7 @@
 qed "hyps_finite";
 
 Goal "hyps p t <= (UN v. {#v, #v->false})";
-by (PropLog.pl.induct_tac "p" 1);
+by (induct_tac "p" 1);
 by (ALLGOALS Simp_tac);
 by (Blast_tac 1);
 qed "hyps_subset";
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Induct/PropLog.thy
--- a/src/HOL/Induct/PropLog.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Induct/PropLog.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -6,7 +6,8 @@
 Inductive definition of propositional logic.
 *)
 
-PropLog = Finite +
+PropLog = Finite + Datatype +
+
 datatype
     'a pl = false | var 'a ("#_" [1000]) | "->" ('a pl) ('a pl) (infixr 90)
 consts
@@ -32,12 +33,12 @@
   sat_def  "H |= p  ==  (!tt. (!q:H. tt[q]) --> tt[p])"
   eval_def "tt[p] == eval2 p tt"
 
-primrec eval2 pl
+primrec
   "eval2(false) = (%x. False)"
   "eval2(#v) = (%tt. v:tt)"
   "eval2(p->q) = (%tt. eval2 p tt-->eval2 q tt)"
 
-primrec hyps pl
+primrec
   "hyps(false) = (%tt.{})"
   "hyps(#v) = (%tt.{if v:tt then #v else #v->false})"
   "hyps(p->q) = (%tt. hyps p tt Un hyps q tt)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -106,7 +106,7 @@
 
 qed_goal "integ_of_bin_norm_Bcons" Bin.thy
     "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)"
- (fn _ =>[(bin.induct_tac "w" 1),
+ (fn _ =>[(induct_tac "w" 1),
           (ALLGOALS Simp_tac) ]);
 
 qed_goal "integ_of_bin_succ" Bin.thy
@@ -140,11 +140,11 @@
 
 Goal
     "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
-by (bin.induct_tac "v" 1);
+by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (rtac allI 1);
-by (bin.induct_tac "w" 1);
+by (induct_tac "w" 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
@@ -162,7 +162,7 @@
                       integ_of_bin_norm_Bcons];
 
 Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w";
-by (bin.induct_tac "v" 1);
+by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (simp_tac (simpset() addsimps bin_mult_simps) 1);
 by (cut_inst_tac [("P","bool")] True_or_False 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Integ/Bin.thy
--- a/src/HOL/Integ/Bin.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Bin.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -22,7 +22,7 @@
 quoting the previously computed values.  (Or code an oracle...)
 *)
 
-Bin = Integ + 
+Bin = Integ + Datatype +
 
 syntax
   "_Int"           :: xnum => int        ("_")
@@ -43,42 +43,42 @@
 
 (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
 
-primrec norm_Bcons bin
+primrec
   norm_Plus  "norm_Bcons PlusSign  b = (if b then (Bcons PlusSign b) else PlusSign)"
   norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign b))"
   norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
  
-primrec integ_of_bin bin
+primrec
   iob_Plus  "integ_of_bin PlusSign = $#0"
   iob_Minus "integ_of_bin MinusSign = $~($#1)"
   iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" 
 
-primrec bin_succ bin
+primrec
   succ_Plus  "bin_succ PlusSign = Bcons PlusSign True" 
   succ_Minus "bin_succ MinusSign = PlusSign"
   succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
 
-primrec bin_pred bin
+primrec
   pred_Plus  "bin_pred(PlusSign) = MinusSign"
   pred_Minus "bin_pred(MinusSign) = Bcons MinusSign False"
   pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
  
-primrec bin_minus bin
+primrec
   min_Plus  "bin_minus PlusSign = PlusSign"
   min_Minus "bin_minus MinusSign = Bcons PlusSign True"
   min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
 
-primrec bin_add bin
+primrec
   add_Plus  "bin_add PlusSign w = w"
   add_Minus "bin_add MinusSign w = bin_pred w"
   add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
 
-primrec bin_mult bin
+primrec
   mult_Plus "bin_mult PlusSign w = PlusSign"
   mult_Minus "bin_mult MinusSign w = bin_minus w"
   mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))"
 
-primrec h_bin bin
+primrec
   h_Plus  "h_bin v x PlusSign =  Bcons v x"
   h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)"
   h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Integ/Integ.ML
--- a/src/HOL/Integ/Integ.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Integ/Integ.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -173,12 +173,12 @@
 (**** zmagnitude: magnitide of an integer, as a natural number ****)
 
 goal Arith.thy "!!n::nat. n - Suc(n+m)=0";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_Suc_add_0";
 
 goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)";
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_Suc_add_inverse";
 
@@ -785,7 +785,7 @@
 
 Goal "$~ $#  n <= $#0";
   by (rtac zless_or_eq_imp_zle 1); 
-  by (nat_ind_tac "n" 1); 
+  by (induct_tac "n" 1); 
   by (ALLGOALS Asm_simp_tac); 
 qed "negative_zle_0"; 
 Addsimps[negative_zle_0]; 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lambda/Eta.ML
--- a/src/HOL/Lambda/Eta.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Eta.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -25,7 +25,7 @@
 section "eta, subst and free";
 
 Goal "!i t u. ~free s i --> s[t/i] = s[u/i]";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
 by (ALLGOALS(simp_tac (addsplit (simpset()))));
 by (Blast_tac 1);
 by (Blast_tac 1);
@@ -33,10 +33,10 @@
 Addsimps [subst_not_free RS eqTrueI];
 
 Goal "!i k. free (lift t k) i = (i < k & free t i | k < i & free t (i-1))";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_full_simp_tac (addsplit (simpset()) addcongs [conj_cong])));
 by (Blast_tac 2);
-by (simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1);
+by (simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1);
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed "free_lift";
@@ -44,12 +44,12 @@
 
 Goal "!i k t. free (s[t/k]) i = \
 \              (free s k & free t i | free s (if i<k then i else Suc i))";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
 by (Asm_simp_tac 2);
 by (Blast_tac 2);
 by (asm_full_simp_tac (addsplit (simpset())) 2);
 by (simp_tac (simpset() addsimps [diff_Suc,subst_Var]
-                      addsplits [split_nat_case]) 1);
+                      addsplits [nat.split]) 1);
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
 qed "free_subst";
@@ -123,7 +123,7 @@
 AddIs [beta_subst];
 
 Goal "!i. t[Var i/i] = t[Var(i)/Suc i]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (addsplit (simpset()))));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
 by (ALLGOALS trans_tac);
@@ -137,7 +137,7 @@
 Addsimps [eta_lift];
 
 Goal "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
-by (dB.induct_tac "u" 1);
+by (induct_tac "u" 1);
 by (ALLGOALS(asm_simp_tac (addsplit (simpset()))));
 by (blast_tac (claset() addIs [r_into_rtrancl]) 1);
 by (blast_tac (claset() addSIs [rtrancl_eta_App]) 1);
@@ -166,7 +166,7 @@
 section "Implicit definition of -e>: Abs(lift s 0 $ Var 0) -e> s";
 
 Goal "!i. (~free s i) = (? t. s = lift t i)";
-by (dB.induct_tac "s" 1);
+by (induct_tac "s" 1);
   by (Simp_tac 1);
   by (SELECT_GOAL(safe_tac HOL_cs)1);
    by (etac nat_neqE 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lambda/Eta.thy
--- a/src/HOL/Lambda/Eta.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Eta.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -19,7 +19,7 @@
   "s -e>= t" == "(s,t) : eta^="
   "s ->=  t" == "(s,t) : beta^="
 
-primrec free Lambda.dB
+primrec
   "free (Var j) i = (j=i)"
   "free (s $ t) i = (free s i | free t i)"
   "free (Abs s) i = free s (Suc i)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lambda/Lambda.ML
--- a/src/HOL/Lambda/Lambda.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Lambda.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -66,16 +66,16 @@
 
 Goal
   "!i k. i < Suc k --> lift (lift t i) (Suc k) = lift (lift t k) i";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
 qed_spec_mp "lift_lift";
 
 Goal "!i j s. j < Suc i --> lift (t[s/j]) i = (lift t (Suc i)) [lift s i / j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [diff_Suc,subst_Var,lift_lift]
-                                addsplits [split_nat_case]
+                                addsplits [nat.split]
                                 addSolver cut_trans_tac)));
 by (safe_tac HOL_cs);
 by (ALLGOALS trans_tac);
@@ -84,7 +84,7 @@
 
 Goal
   "!i j s. i < Suc j --> lift (t[s/j]) i = (lift t i) [lift s i / Suc j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac (simpset() addsimps [subst_Var,lift_lift]
                                 addSolver cut_trans_tac)));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -92,18 +92,18 @@
 qed "lift_subst_lt";
 
 Goal "!k s. (lift t k)[s/k] = t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_lift";
 Addsimps [subst_lift];
 
 
 Goal "!i j u v. i < Suc j --> t[lift v i / Suc j][u[v/j]/i] = t[u/i][v/j]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac
       (simpset() addsimps [diff_Suc,subst_Var,lift_lift RS sym,lift_subst_lt]
                  delsplits [split_if]
-                 addsplits [split_nat_case]
+                 addsplits [nat.split]
                  addloop ("if",split_inside_tac[split_if])
                 addSolver cut_trans_tac)));
 by (safe_tac (HOL_cs addSEs [nat_neqE]));
@@ -114,20 +114,20 @@
 (*** Equivalence proof for optimized substitution ***)
 
 Goal "!k. liftn 0 t k = t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 qed "liftn_0";
 Addsimps [liftn_0];
 
 Goal "!k. liftn (Suc n) t k = lift (liftn n t k) k";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 by (blast_tac (claset() addDs [add_lessD1]) 1);
 qed "liftn_lift";
 Addsimps [liftn_lift];
 
 Goal "!n. substn t s n = t[liftn n s 0 / n]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(asm_simp_tac(addsplit(simpset()))));
 qed "substn_subst_n";
 Addsimps [substn_subst_n];
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
 substitution and beta-reduction.
 *)
 
-Lambda = Arith + Inductive +
+Lambda = Datatype +
 
 datatype dB = Var nat | "$" dB dB (infixl 200) | Abs dB
 
@@ -18,23 +18,23 @@
   substn :: [dB,dB,nat] => dB
   liftn  :: [nat,dB,nat] => dB
 
-primrec lift dB
+primrec
   "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
   "lift (s $ t) k = (lift s k) $ (lift t k)"
   "lift (Abs s) k = Abs(lift s (Suc k))"
 
-primrec subst dB
+primrec
   subst_Var "(Var i)[s/k] = (if k < i then Var(i-1)
                             else if i = k then s else Var i)"
   subst_App "(t $ u)[s/k] = t[s/k] $ u[s/k]"
   subst_Abs "(Abs t)[s/k] = Abs (t[lift s 0 / Suc k])"
 
-primrec liftn dB
+primrec
   "liftn n (Var i) k = (if i < k then Var i else Var(i+n))"
   "liftn n (s $ t) k = (liftn n s k) $ (liftn n t k)"
   "liftn n (Abs s) k = Abs(liftn n s (Suc k))"
 
-primrec substn dB
+primrec
   "substn (Var i) s k = (if k < i then Var(i-1)
                          else if i = k then liftn k s 0 else Var i)"
   "substn (t $ u) s k = (substn t s k) $ (substn u s k)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lambda/ParRed.ML
--- a/src/HOL/Lambda/ParRed.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lambda/ParRed.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -26,7 +26,7 @@
 Addsimps [par_beta_varL];
 
 Goal "t => t";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"par_beta_refl";
 Addsimps [par_beta_refl];
@@ -52,14 +52,14 @@
 (*** => ***)
 
 Goal "!t' n. t => t' --> lift t n => lift t' n";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(fast_tac (claset() addss (simpset()))));
 qed_spec_mp "par_beta_lift";
 Addsimps [par_beta_lift];
 
 Goal
   "!s s' t' n. s => s' --> t => t' --> t[s/n] => t'[s'/n]";
-by (dB.induct_tac "t" 1);
+by (induct_tac "t" 1);
   by (asm_simp_tac (addsplit(simpset())) 1);
  by (strip_tac 1);
  by (eresolve_tac par_beta_cases 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/AutoChopper.thy
--- a/src/HOL/Lex/AutoChopper.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/AutoChopper.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -29,7 +29,8 @@
 consts
   acc :: "[('a,'s)da, 's, 'a list list*'a list, 'a list, 'a list, 'a list]
           => 'a list list * 'a list"
-primrec acc List.list
+
+primrec
   "acc A s r ps []     zs = (if ps=[] then r else (ps#fst(r),snd(r)))" 
   "acc A s r ps (x#xs) zs =
             (let t = next A x s
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/AutoMaxChop.thy
--- a/src/HOL/Lex/AutoMaxChop.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
 
 consts
  auto_split :: "('a,'s)da => 's  => 'a list * 'a list => 'a list => 'a splitter"
-primrec auto_split list
+primrec
 "auto_split A q res ps []     = (if fin A q then (ps,[]) else res)"
 "auto_split A q res ps (x#xs) =
    auto_split A (next A x q) (if fin A q then (ps,x#xs) else res) (ps@[x]) xs"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -84,7 +84,7 @@
                         addsplits [split_split]) 1);
 by (Clarify_tac 1);
 by (rename_tac "xs1 ys1 xss1 ys" 1);
-by (split_asm_tac [split_list_case_asm] 1);
+by (split_asm_tac [list.split_asm] 1);
  by (Asm_full_simp_tac 1);
  by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
  by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/MaxPrefix.thy
--- a/src/HOL/Lex/MaxPrefix.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -19,7 +19,7 @@
 
 consts
  maxsplit :: "('a list => bool) => 'a list * 'a list => 'a list => 'a splitter"
-primrec maxsplit list
+primrec
 "maxsplit P res ps []     = (if P ps then (ps,[]) else res)"
 "maxsplit P res ps (q#qs) = maxsplit P (if P ps then (ps,q#qs) else res)
                                      (ps@[q]) qs"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/NA.thy
--- a/src/HOL/Lex/NA.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/NA.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
 types ('a,'s)na = "'s * ('a => 's => 's set) * ('s => bool)"
 
 consts delta :: "('a,'s)na => 'a list => 's => 's set"
-primrec delta list
+primrec
 "delta A []    p = {p}"
 "delta A (a#w) p = Union(delta A w `` next A a p)"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/NAe.thy
--- a/src/HOL/Lex/NAe.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/NAe.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
 translations "eps A" == "step A None"
 
 consts steps :: "('a,'s)nae => 'a list =>   ('s * 's)set"
-primrec steps list
+primrec
 "steps A [] = (eps A)^*"
 "steps A (a#w) = steps A w  O  step A (Some a)  O  (eps A)^*"
 
@@ -28,7 +28,7 @@
 
 (* not really used:
 consts delta :: "('a,'s)nae => 'a list => 's => 's set"
-primrec delta list
+primrec
 "delta A [] s = (eps A)^* ^^ {s}"
 "delta A (a#w) s = lift(delta A w) (lift(next A (Some a)) ((eps A)^* ^^ {s}))"
 *)
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
 (* Junk: *)
 val [maj,min] = goal Prefix.thy "[| Q([]); !! y ys. Q(y#ys) |] ==> ! l. Q(l)";
 by (rtac allI 1);
-by (list.induct_tac "l" 1);
+by (induct_tac "l" 1);
 by (rtac maj 1);
 by (rtac min 1);
 val list_cases = result();
@@ -37,7 +37,7 @@
 AddIffs[Nil_prefix];
 
 Goalw [prefix_def] "(xs <= []) = (xs = [])";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 qed "prefix_Nil";
@@ -83,7 +83,7 @@
 (* nicht sehr elegant bewiesen - Induktion eigentlich ueberfluessig *)
 Goalw [prefix_def]
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/RegExp.thy
--- a/src/HOL/Lex/RegExp.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -15,7 +15,7 @@
                  | Star ('a rexp)
 
 consts lang :: 'a rexp => 'a list set
-primrec lang rexp
+primrec
 lang_Emp  "lang Empty = {}"
 lang_Atom "lang (Atom a) = {[a]}"
 lang_Un   "lang (Union el er) = (lang el) Un (lang er)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -446,7 +446,7 @@
 
 Goalw [conc_def]
  "!L R. fin(conc L R) p = (? s. p = False#s & fin R s)";
-by (simp_tac (simpset() addsplits [split_list_case]) 1);
+by (simp_tac (simpset() addsplits [list.split]) 1);
 qed_spec_mp "final_conc";
 
 Goal
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/RegExp2NAe.thy
--- a/src/HOL/Lex/RegExp2NAe.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -50,7 +50,7 @@
     %s. case s of [] => True | left#s => left & f s)"
 
 consts rexp2nae :: 'a rexp => 'a bitsNAe
-primrec rexp2nae rexp
+primrec
 "rexp2nae Empty      = ([], %a s. {}, %s. False)"
 "rexp2nae(Atom a)    = atom a"
 "rexp2nae(Union r s) = union (rexp2nae r) (rexp2nae s)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -140,7 +140,7 @@
  "!i j xs. xs : regset d i j k = \
 \          ((!n:set(butlast(trace d i xs)). n < k) & deltas d xs i = j)";
 by (induct_tac "k" 1);
- by (simp_tac (simpset() addcongs [conj_cong] addsplits [split_list_case]) 1);
+ by (simp_tac (simpset() addcongs [conj_cong] addsplits [list.split]) 1);
 by (strip_tac 1);
 by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
 by (rtac iffI 1);
@@ -149,12 +149,12 @@
  by (REPEAT(eresolve_tac[exE,conjE] 1));
  by (Asm_full_simp_tac 1);
  by (subgoal_tac
-      "(!n:set(butlast(trace d k xsb)). n < Suc k) & deltas d xsb k = k" 1);
+      "(!m:set(butlast(trace d n xsb)). m < Suc n) & deltas d xsb n = n" 1);
   by (asm_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
  by (etac star.induct 1);
   by (Simp_tac 1);
  by (asm_full_simp_tac (simpset() addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
-by (case_tac "k : set(butlast(trace d i xs))" 1);
+by (case_tac "n : set(butlast(trace d i xs))" 1);
  by (rtac disjI1 2);
  by (blast_tac (claset() addIs [lemma]) 2);
 by (rtac disjI2 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Lex/RegSet_of_nat_DA.thy
--- a/src/HOL/Lex/RegSet_of_nat_DA.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -23,14 +23,14 @@
 translations "deltas" == "foldl2"
 
 consts trace :: 'a nat_next => nat => 'a list => nat list
-primrec trace list
+primrec
 "trace d i [] = []"
 "trace d i (x#xs) = d x i # trace d (d x i) xs"
 
 (* conversion a la Warshall *)
 
 consts regset :: 'a nat_next => nat => nat => nat => 'a list set
-primrec regset nat
+primrec
 "regset d i j 0 = (if i=j then insert [] {[a] | a. d a i = j}
                           else {[a] | a. d a i = j})"
 "regset d i j (Suc k) = regset d i j k Un
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Generalize.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -7,12 +7,12 @@
 AddSEs [equalityE];
 
 Goal "free_tv A = free_tv B ==> gen A t = gen B t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "gen_eq_on_free_tv";
 
 Goal "(free_tv t) <= (free_tv sch) --> gen sch t = (mk_scheme t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Asm_simp_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
@@ -21,7 +21,7 @@
 Addsimps [gen_without_effect];
 
 Goal "free_tv (gen ($ S A) t) = free_tv t Int free_tv ($ S A)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv ($ S A)" 1);
 by (Asm_simp_tac 1);
@@ -42,7 +42,7 @@
 Addsimps [free_tv_gen_cons];
 
 Goal "bound_tv (gen A t1) = (free_tv t1) - (free_tv A)";
-by (typ.induct_tac "t1" 1);
+by (induct_tac "t1" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
 by (Asm_simp_tac 1);
@@ -55,7 +55,7 @@
 Addsimps [bound_tv_gen];
 
 Goal "new_tv n t --> new_tv n (gen A t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
 by (Asm_simp_tac 1);
@@ -63,7 +63,7 @@
 qed_spec_mp "new_tv_compatible_gen";
 
 Goalw [gen_ML_def] "gen A t = gen_ML A t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme_list]) 1);
 qed "gen_eq_gen_ML";
@@ -85,7 +85,7 @@
 qed_spec_mp "gen_subst_commutes";
 
 Goal "free_tv(t::typ) <= free_tv(A) --> bound_typ_inst S (gen A t) = t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Fast_tac 1);
 qed_spec_mp "bound_typ_inst_gen";
@@ -96,7 +96,7 @@
 by Safe_tac;
 by (rename_tac "R" 1);
 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
  by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "gen_bound_typ_instance";
@@ -106,7 +106,7 @@
 by Safe_tac;
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
  by (Asm_simp_tac 1);
  by (Fast_tac 1);
 by (Asm_simp_tac 1);
@@ -119,7 +119,7 @@
 by (etac exE 1);
 by (hyp_subst_tac 1);
 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
 by (Asm_simp_tac 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Generalize.thy
--- a/src/HOL/MiniML/Generalize.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Generalize.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -16,7 +16,7 @@
 consts
   gen :: [ctxt, typ] => type_scheme
 
-primrec gen typ
+primrec
   "gen A (TVar n) = (if (n:(free_tv A)) then (FVar n) else (BVar n))"
   "gen A (t1 -> t2) = (gen A t1) =-> (gen A t2)"
 
@@ -25,7 +25,7 @@
 consts
   gen_ML_aux :: [nat list, typ] => type_scheme
 
-primrec gen_ML_aux typ
+primrec
   "gen_ML_aux A (TVar n) = (if (n mem A) then (FVar n) else (BVar n))"
   "gen_ML_aux A (t1 -> t2) = (gen_ML_aux A t1) =-> (gen_ML_aux A t2)"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Instance.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -10,14 +10,14 @@
 (* lemmatas for bound_typ_inst *)
 
 Goal "bound_typ_inst S (mk_scheme t) = t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bound_typ_inst_mk_scheme";
 
 Addsimps [bound_typ_inst_mk_scheme];
 
 Goal "bound_typ_inst ($S o R) ($S sch) = $S (bound_typ_inst R sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "bound_typ_inst_composed_subst";
 
@@ -32,7 +32,7 @@
 (* lemmatas for bound_scheme_inst *)
 
 Goal "bound_scheme_inst B (mk_scheme t) = mk_scheme t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
 qed "bound_scheme_inst_mk_scheme";
@@ -40,7 +40,7 @@
 Addsimps [bound_scheme_inst_mk_scheme];
 
 Goal "$S (bound_scheme_inst B sch) = (bound_scheme_inst ($S o B) ($ S sch))";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -48,7 +48,7 @@
 
 Goal "!t. mk_scheme t = bound_scheme_inst B sch --> \
 \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by Safe_tac;
 by (rtac exI 1);
@@ -81,7 +81,7 @@
 
 Goal "new_tv n sch --> subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) \
 \                                                 (bound_typ_inst (%k. TVar (k + n)) sch) = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (simp_tac (simpset() addsimps [leD]) 1);
 by (simp_tac (simpset() addsimps [le_add2,diff_add_inverse2]) 1);
 by (Asm_simp_tac 1);
@@ -96,7 +96,7 @@
 Goal "new_tv n sch --> \
 \     subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k) (bound_typ_inst S sch) = \
 \      bound_scheme_inst ((subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S) sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (simp_tac (simpset() addsimps [leD]) 1);
 by (Asm_simp_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [leD]) 1);
@@ -127,7 +127,7 @@
 by (asm_simp_tac (simpset() addsimps [aux2]) 1);
 by Safe_tac;
 by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Asm_simp_tac 1);
@@ -145,7 +145,7 @@
 by (rotate_tac 1 1);
 by (rtac mp 1);
 by (assume_tac 2);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Fast_tac 1);
@@ -154,7 +154,7 @@
 by (etac exE 1);
 by (Asm_full_simp_tac 1);
 by (rtac exI 1);
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -172,7 +172,7 @@
 by (rtac conjI 1);
  by (Fast_tac 1);
 by (rtac allI 1);
-by (nat_ind_tac "i" 1);
+by (induct_tac "i" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "le_env_Cons";
 AddIffs [le_env_Cons];
@@ -221,7 +221,7 @@
 
 Goalw [le_type_scheme_def,is_bound_typ_instance]
  "(sch <= FVar n) = (sch = FVar n)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
  by (Fast_tac 1);
@@ -249,26 +249,26 @@
 qed "Fun_le_FunD";
 
 Goal "(sch' <= sch1 =-> sch2) --> (? sch'1 sch'2. sch' = sch'1 =-> sch'2)";
-by (type_scheme.induct_tac "sch'" 1);
+by (induct_tac "sch'" 1);
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
 by (Fast_tac 1);
 qed_spec_mp "scheme_le_Fun";
 
 Goal "!sch'::type_scheme. sch <= sch' --> free_tv sch' <= free_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
   by (rtac allI 1);
-  by (type_scheme.induct_tac "sch'" 1);
+  by (induct_tac "sch'" 1);
     by (Simp_tac 1);
    by (Simp_tac 1);
   by (Simp_tac 1);
  by (rtac allI 1);
- by (type_scheme.induct_tac "sch'" 1);
+ by (induct_tac "sch'" 1);
    by (Simp_tac 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
 by (rtac allI 1);
-by (type_scheme.induct_tac "sch'" 1);
+by (induct_tac "sch'" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -278,10 +278,10 @@
 qed_spec_mp "le_type_scheme_free_tv";
 
 Goal "!A::type_scheme list. A <= B --> free_tv B <= free_tv A";
-by (list.induct_tac "B" 1);
+by (induct_tac "B" 1);
  by (Simp_tac 1);
 by (rtac allI 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
  by (simp_tac (simpset() addsimps [le_env_def]) 1);
 by (Simp_tac 1);
 by (fast_tac (claset() addDs [le_type_scheme_free_tv]) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Instance.thy
--- a/src/HOL/MiniML/Instance.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Instance.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -14,7 +14,7 @@
 consts
   bound_typ_inst :: [subst, type_scheme] => typ
 
-primrec bound_typ_inst type_scheme
+primrec
   "bound_typ_inst S (FVar n) = (TVar n)"
   "bound_typ_inst S (BVar n) = (S n)"
   "bound_typ_inst S (sch1 =-> sch2) = ((bound_typ_inst S sch1) -> (bound_typ_inst S sch2))"
@@ -22,7 +22,7 @@
 consts
   bound_scheme_inst :: [nat => type_scheme, type_scheme] => type_scheme
 
-primrec bound_scheme_inst type_scheme
+primrec
   "bound_scheme_inst S (FVar n) = (FVar n)"
   "bound_scheme_inst S (BVar n) = (S n)"
   "bound_scheme_inst S (sch1 =-> sch2) = ((bound_scheme_inst S sch1) =-> (bound_scheme_inst S sch2))"
@@ -38,7 +38,7 @@
 consts
   subst_to_scheme :: [nat => type_scheme, typ] => type_scheme
 
-primrec subst_to_scheme typ
+primrec
   "subst_to_scheme B (TVar n) = (B n)"
   "subst_to_scheme B (t1 -> t2) = ((subst_to_scheme B t1) =-> (subst_to_scheme B t2))"
   
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Maybe.ML
--- a/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Maybe.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
 (* expansion of option_bind *)
 Goalw [option_bind_def] "P(option_bind res f) = \
 \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
-by (rtac split_option_case 1);
+by (rtac option.split 1);
 qed "split_option_bind";
 
 Goal
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/MiniML.ML
--- a/src/HOL/MiniML/MiniML.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/MiniML.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -47,22 +47,22 @@
 qed "alpha_A";
 
 Goal "$ (S o alpha) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_typ";
 
 Goal "$ (%u. (S o alpha) u) (t::typ) = $ S ($ (%x. TVar (alpha x)) t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 val S_o_alpha_typ' = result ();
 
 Goal "$ (S o alpha) (sch::type_scheme) = $ S ($ (%x. TVar (alpha x)) sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 qed "S_o_alpha_type_scheme";
 
 Goal "$ (S o alpha) (A::type_scheme list) = $ S ($ (%x. TVar (alpha x)) A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 by (rtac (rewrite_rule [o_def] S_o_alpha_type_scheme) 1);
 qed "S_o_alpha_type_scheme_list";
@@ -106,7 +106,7 @@
 Goal "!!t1::typ. \
 \     (free_tv ($ (%x. TVar (if x : free_tv A then x else n + x)) t1) - free_tv A) <= \
 \         {x. ? y. x = n + y}";
-by (typ.induct_tac "t1" 1);
+by (induct_tac "t1" 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
 by (Simp_tac 1);
@@ -143,7 +143,7 @@
 
 Goal "!A::type_scheme list. new_tv n A --> {x. ? y. x = n + y} Int free_tv A = {}";
 by (rtac allI 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (fast_tac (claset() addDs [new_tv_Int_free_tv_empty_scheme ]) 1);
@@ -155,7 +155,7 @@
 by (etac exE 1);
 by (hyp_subst_tac 1);
 by (res_inst_tac [("x","(%x. S (if n <= x then x - n else x))")] exI 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (case_tac "nat : free_tv A" 1);
 by (Asm_simp_tac 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Type.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -10,33 +10,33 @@
 (* lemmata for make scheme *)
 
 Goal "mk_scheme t = sch1 =-> sch2 --> (? t1 t2. sch1 = mk_scheme t1 & sch2 = mk_scheme t2)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (Fast_tac 1);
 qed_spec_mp "mk_scheme_Fun";
 
 Goal "!t'. mk_scheme t = mk_scheme t' --> t=t'";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
  by (rtac allI 1);
- by (typ.induct_tac "t'" 1);
+ by (induct_tac "t'" 1);
   by (Simp_tac 1);
  by (Asm_full_simp_tac 1);
 by (rtac allI 1);
-by (typ.induct_tac "t'" 1);
+by (induct_tac "t'" 1);
  by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "mk_scheme_injective";
 
 Goal "free_tv (mk_scheme t) = free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "free_tv_mk_scheme";
 
 Addsimps [free_tv_mk_scheme];
 
 Goal "$ S (mk_scheme t) = mk_scheme ($ S t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_mk_scheme";
 
@@ -110,14 +110,14 @@
 
 Goal "new_tv n (sch::type_scheme) --> \
 \     $(%k. if k<n then S k else S' k) sch = $S sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme";
 Addsimps [new_if_subst_type_scheme];
 
 Goal "new_tv n (A::type_scheme list) --> \
 \     $(%k. if k<n then S k else S' k) A = $S A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_if_subst_type_scheme_list";
 Addsimps [new_if_subst_type_scheme_list];
@@ -147,7 +147,7 @@
 Addsimps [free_tv_id_subst];
 
 Goal "!n. n < length A --> x : free_tv (A!n) --> x : free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (res_inst_tac [("n","n")] nat_induct 1);
@@ -158,7 +158,7 @@
 Addsimps [free_tv_nth_A_impl_free_tv_A];
 
 Goal "!nat. nat < length A --> x : free_tv (A!nat) --> x : free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (res_inst_tac [("n","nat")] nat_induct 1);
@@ -173,7 +173,7 @@
    occurring in the type structure *)
 
 Goal "(!x:free_tv t. (S x) = (S' x)) --> $ S (t::typ) = $ S' t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed_spec_mp "typ_substitutions_only_on_free_variables";
@@ -184,7 +184,7 @@
 qed "eq_free_eq_subst_te";
 
 Goal "(!x:free_tv sch. (S x) = (S' x)) --> $ S (sch::type_scheme) = $ S' sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
@@ -198,7 +198,7 @@
 
 Goal
   "(!n. n:(free_tv A) --> S1 n = S2 n) --> $S1 (A::type_scheme list) = $S2 A";
-by (list.induct_tac "A" 1); 
+by (induct_tac "A" 1); 
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
@@ -210,7 +210,7 @@
 val weaken_asm_Un = result ();
 
 Goal "(!x:free_tv A. (S x) = (S' x)) --> $ S (A::type_scheme list) = $ S' A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (rtac weaken_asm_Un 1);
@@ -220,7 +220,7 @@
 
 Goal
   "$ S1 (t::typ) = $ S2 t --> n:(free_tv t) --> S1 n = S2 n";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Fun t1 t2 *)
@@ -229,7 +229,7 @@
 
 Goal
   "$ S1 (sch::type_scheme) = $ S2 sch --> n:(free_tv sch) --> S1 n = S2 n";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 (* case TVar n *)
 by (Asm_simp_tac 1);
 (* case BVar n *)
@@ -242,7 +242,7 @@
 
 Goal
   "$S1 (A::type_scheme list) = $S2 A --> n:(free_tv A) --> S1 n = S2 n";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
@@ -281,7 +281,7 @@
 qed "free_tv_subst_var";
 
 Goal "free_tv ($ S (t::typ)) <= cod S Un free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
@@ -289,7 +289,7 @@
 qed "free_tv_app_subst_te";     
 
 Goal "free_tv ($ S (sch::type_scheme)) <= cod S Un free_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 (* case FVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
 (* case BVar n *)
@@ -299,7 +299,7 @@
 qed "free_tv_app_subst_type_scheme";  
 
 Goal "free_tv ($ S (A::type_scheme list)) <= cod S Un free_tv A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -322,14 +322,14 @@
 qed "free_tv_o_subst";
 
 Goal "n : free_tv t --> free_tv (S n) <= free_tv ($ S t::typ)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Fast_tac 1);
 qed_spec_mp "free_tv_of_substitutions_extend_to_types";
 
 Goal "n : free_tv sch --> free_tv (S n) <= free_tv ($ S sch::type_scheme)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -337,7 +337,7 @@
 qed_spec_mp "free_tv_of_substitutions_extend_to_schemes";
 
 Goal "n : free_tv A --> free_tv (S n) <= free_tv ($ S A::type_scheme list)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_schemes]) 1);
@@ -346,14 +346,14 @@
 Addsimps [free_tv_of_substitutions_extend_to_scheme_lists];
 
 Goal "!!sch::type_scheme. (n : free_tv sch) = (n mem free_tv_ML sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 by (strip_tac 1);
 by (Fast_tac 1);
 qed "free_tv_ML_scheme";
 
 Goal "!!A::type_scheme list. (n : free_tv A) = (n mem free_tv_ML A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [free_tv_ML_scheme]) 1);
 qed "free_tv_ML_scheme_list";
@@ -362,14 +362,14 @@
 (* lemmata for bound_tv *)
 
 Goal "bound_tv (mk_scheme t) = {}";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bound_tv_mk_scheme";
 
 Addsimps [bound_tv_mk_scheme];
 
 Goal "!!sch::type_scheme. bound_tv ($ S sch) = bound_tv sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bound_tv_subst_scheme";
 
@@ -410,28 +410,28 @@
 Goal 
   "new_tv n  = list_all (new_tv n)";
 by (rtac ext 1);
-by (list.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
 
 (* substitution affects only variables occurring freely *)
 Goal
   "new_tv n (t::typ) --> $(%x. if x=n then t' else S x) t = $S t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
 Goal
   "new_tv n (sch::type_scheme) --> $(%x. if x=n then sch' else S x) sch = $S sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "subst_te_new_type_scheme";
 Addsimps [subst_te_new_type_scheme];
 
 Goal
   "new_tv n (A::type_scheme list) --> $(%x. if x=n then t else S x) A = $S A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "subst_tel_new_scheme_list";
 Addsimps [subst_tel_new_scheme_list];
@@ -466,13 +466,13 @@
 
 Goal
   "new_tv n S --> new_tv n (t::typ) --> new_tv n ($ S t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_te";
 Addsimps [new_tv_subst_te];
 
 Goal "new_tv n S --> new_tv n (sch::type_scheme) --> new_tv n ($ S sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS (Asm_full_simp_tac));
 by (rewtac new_tv_def);
 by (simp_tac (simpset() addsimps [free_tv_subst,dom_def,cod_def]) 1);
@@ -487,7 +487,7 @@
 
 Goal
   "new_tv n S --> new_tv n (A::type_scheme list) --> new_tv n ($ S A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (simpset()))));
 qed_spec_mp "new_tv_subst_scheme_list";
 Addsimps [new_tv_subst_scheme_list];
@@ -495,7 +495,7 @@
 Goal
   "new_tv n A --> new_tv (Suc n) ((TVar n)#A)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
 
@@ -509,7 +509,7 @@
 
 Goalw [new_tv_def]
   "!nat. nat < length A --> new_tv n A --> (new_tv n (A!nat))";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (res_inst_tac [("n","nat")] nat_induct 1);
@@ -549,7 +549,7 @@
 val less_maxR = result();
 
 Goalw [new_tv_def] "!!t::typ. ? n. (new_tv n t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (res_inst_tac [("x","Suc nat")] exI 1);
 by (Asm_simp_tac 1);
 by (REPEAT (etac exE 1));
@@ -562,7 +562,7 @@
 Addsimps [fresh_variable_types];
 
 Goalw [new_tv_def] "!!sch::type_scheme. ? n. (new_tv n sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (res_inst_tac [("x","Suc nat")] exI 1);
 by (Simp_tac 1);
 by (res_inst_tac [("x","Suc nat")] exI 1);
@@ -586,7 +586,7 @@
 val le_maxR = result();
 
 Goal "!!A::type_scheme list. ? n. (new_tv n A)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Simp_tac 1);
 by (Simp_tac 1);
 by (etac exE 1);
@@ -648,7 +648,7 @@
 Addsimps [length_app_subst_list];
 
 Goal "!!sch::type_scheme. $ TVar sch = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_TVar_scheme";
 
@@ -665,7 +665,7 @@
 Goalw [id_subst_def]
   "$ id_subst = (%t::typ. t)";
 by (rtac ext 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_te";
 Addsimps [app_subst_id_te];
@@ -673,7 +673,7 @@
 Goalw [id_subst_def]
   "$ id_subst = (%sch::type_scheme. sch)";
 by (rtac ext 1);
-by (type_scheme.induct_tac "t" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_type_scheme";
 Addsimps [app_subst_id_type_scheme];
@@ -682,20 +682,20 @@
 Goalw [app_subst_list]
   "$ id_subst = (%A::type_scheme list. A)";
 by (rtac ext 1); 
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_tel";
 Addsimps [app_subst_id_tel];
 
 Goal "!!sch::type_scheme. $ id_subst sch = sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [id_subst_def])));
 qed "id_subst_sch";
 
 Addsimps [id_subst_sch];
 
 Goal "!!A::type_scheme list. $ id_subst A = A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed "id_subst_A";
@@ -710,18 +710,18 @@
 Addsimps[o_id_subst];
 
 Goal "$ R ($ S t::typ) = $ (%x. $ R (S x) ) t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_comp_te";
 
 Goal "$ R ($ S sch::type_scheme) = $ (%x. $ R (S x) ) sch";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_comp_type_scheme";
 
 Goalw [app_subst_list]
   "$ R ($ S A::type_scheme list) = $ (%x. $ R (S x)) A";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -740,7 +740,7 @@
 qed "subst_id_on_type_scheme_list";
 
 Goal "!n. n < length A --> ($ S A)!n = $S (A!n)";
-by (list.induct_tac "A" 1);
+by (induct_tac "A" 1);
 by (Asm_full_simp_tac 1);
 by (rtac allI 1);
 by (rename_tac "n1" 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/Type.thy
--- a/src/HOL/MiniML/Type.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/Type.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -25,7 +25,7 @@
 consts
   mk_scheme :: typ => type_scheme
 
-primrec mk_scheme typ
+primrec
   "mk_scheme (TVar n) = (FVar n)"
   "mk_scheme (t1 -> t2) = ((mk_scheme t1) =-> (mk_scheme t2))"
 
@@ -41,16 +41,16 @@
 consts
   free_tv :: ['a::type_struct] => nat set
 
-primrec free_tv typ
+primrec
   free_tv_TVar    "free_tv (TVar m) = {m}"
   free_tv_Fun     "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
 
-primrec free_tv type_scheme
+primrec
   "free_tv (FVar m) = {m}"
   "free_tv (BVar m) = {}"
   "free_tv (S1 =-> S2) = (free_tv S1) Un (free_tv S2)"
 
-primrec free_tv list
+primrec
   "free_tv [] = {}"
   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
@@ -59,12 +59,12 @@
 consts
   free_tv_ML :: ['a::type_struct] => nat list
 
-primrec free_tv_ML type_scheme
+primrec
   "free_tv_ML (FVar m) = [m]"
   "free_tv_ML (BVar m) = []"
   "free_tv_ML (S1 =-> S2) = (free_tv_ML S1) @ (free_tv_ML S2)"
 
-primrec free_tv_ML list
+primrec
   "free_tv_ML [] = []"
   "free_tv_ML (x#l) = (free_tv_ML x) @ (free_tv_ML l)"
 
@@ -82,12 +82,12 @@
 consts
   bound_tv :: ['a::type_struct] => nat set
 
-primrec bound_tv type_scheme
+primrec
   "bound_tv (FVar m) = {}"
   "bound_tv (BVar m) = {m}"
   "bound_tv (S1 =-> S2) = (bound_tv S1) Un (bound_tv S2)"
 
-primrec bound_tv list
+primrec
   "bound_tv [] = {}"
   "bound_tv (x#l) = (bound_tv x) Un (bound_tv l)"
 
@@ -97,7 +97,7 @@
 consts
   min_new_bound_tv :: 'a::type_struct => nat
 
-primrec min_new_bound_tv type_scheme
+primrec
   "min_new_bound_tv (FVar n) = 0"
   "min_new_bound_tv (BVar n) = Suc n"
   "min_new_bound_tv (sch1 =-> sch2) = max (min_new_bound_tv sch1) (min_new_bound_tv sch2)"
@@ -118,11 +118,11 @@
 consts
   app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-primrec app_subst typ 
+primrec
   app_subst_TVar "$ S (TVar n) = S n" 
   app_subst_Fun  "$ S (t1 -> t2) = ($ S t1) -> ($ S t2)" 
 
-primrec app_subst type_scheme
+primrec
   "$ S (FVar n) = mk_scheme (S n)"
   "$ S (BVar n) = (BVar n)"
   "$ S (sch1 =-> sch2) = ($ S sch1) =-> ($ S sch2)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/W.ML
--- a/src/HOL/MiniML/W.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/W.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -16,7 +16,7 @@
 (* the resulting type variable is always greater or equal than the given one *)
 Goal
         "!A n S t m. W e A n  = Some (S,t,m) --> n<=m";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var(n) *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 (* case Abs e *)
@@ -45,7 +45,7 @@
 qed "new_tv_compatible_W";
 
 Goal "new_tv n sch --> new_tv (n + (min_new_bound_tv sch)) (bound_typ_inst (%b. TVar (b + n)) sch)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
   by (Asm_full_simp_tac 1);
  by (asm_full_simp_tac (simpset() addsimps [add_commute]) 1);
 by (strip_tac 1);
@@ -74,7 +74,7 @@
 Goal
      "!n A S t m. new_tv n A --> W e A n = Some (S,t,m) -->    \
 \                 new_tv m S & new_tv m t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (simp_tac (simpset() addsplits [split_option_bind]) 1);
 by (strip_tac 1);
@@ -156,7 +156,7 @@
 qed_spec_mp "new_tv_W";
 
 Goal "(v ~: free_tv sch) --> (v : free_tv (bound_typ_inst (TVar o S) sch)) --> (? x. v = S x)";
-by (type_scheme.induct_tac "sch" 1);
+by (induct_tac "sch" 1);
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 by (strip_tac 1);
@@ -170,7 +170,7 @@
 Goal
      "!n A S t m v. W e A n = Some (S,t,m) -->            \
 \         (v:free_tv S | v:free_tv t) --> v<n --> v:free_tv A";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (simp_tac (simpset() addsimps
     [free_tv_subst] addsplits [split_option_bind]) 1);
@@ -265,7 +265,7 @@
 (* correctness of W with respect to has_type *)
 Goal
         "!A S t m n . new_tv n A --> Some (S,t,m) = W e A n --> $S A |- e :: t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (Asm_full_simp_tac 1);
 by (strip_tac 1);
@@ -388,7 +388,7 @@
  "!S' A t' n. $S' A |- e :: t' --> new_tv n A -->     \
 \             (? S t. (? m. W e A n = Some (S,t,m)) &  \
 \                     (? R. $S' A = $R ($S A) & t' = $R t))";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/MiniML/W.thy
--- a/src/HOL/MiniML/W.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/MiniML/W.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -17,7 +17,7 @@
 consts
         W :: [expr, ctxt, nat] => result_W
 
-primrec W expr
+primrec
   "W (Var i) A n =  
      (if i < length A then Some( id_subst,   
 	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Quot/NPAIR.thy
--- a/src/HOL/Quot/NPAIR.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Quot/NPAIR.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -6,11 +6,9 @@
 Example: define a PER on pairs of natural numbers (with embedding)
 
 *)
-NPAIR = PER + Arith + (* representation for rational numbers *)
+NPAIR = PER + Datatype + (* representation for rational numbers *)
 
-types np = "(nat * nat)" (* is needed for datatype *)
-
-datatype NP = abs_NP np
+datatype NP = abs_NP "(nat * nat)"
 
 consts	rep_NP :: "NP => nat * nat"
 
@@ -23,4 +21,4 @@
 (* for proves of this rule see [Slo97diss] *)
 rules
 	per_trans_NP	"[| eqv (x::NP) y;eqv y z |] ==> eqv x z"
-end
\ No newline at end of file
+end
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Real/PNat.ML
--- a/src/HOL/Real/PNat.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Real/PNat.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -48,11 +48,8 @@
 qed "pnat_induct";
 
 (*Perform induction on n. *)
-local fun raw_pnat_ind_tac a i = 
-    res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1)
-in
-val pnat_ind_tac = Datatype.occs_in_prems raw_pnat_ind_tac
-end;
+fun pnat_ind_tac a i = 
+  res_inst_tac [("n",a)] pnat_induct i  THEN  rename_last_tac a [""] (i+1);
 
 val prems = goal thy
     "[| !!x. P x 1p;  \
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Real/Real.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -1267,7 +1267,7 @@
 
 Goal "1r <= %%#n";
 by (simp_tac (simpset() addsimps [real_nat_one RS sym]) 1);
-by (nat_ind_tac "n" 1);
+by (induct_tac "n" 1);
 by (auto_tac (claset(),simpset () 
     addsimps [real_nat_Suc,real_le_refl,real_nat_one]));
 by (res_inst_tac [("t","1r")] (real_add_zero_left RS subst) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Subst/Subst.thy
--- a/src/HOL/Subst/Subst.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/Subst.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -18,7 +18,7 @@
   srange ::  "('a*('a uterm)) list => 'a set"
 
 
-primrec "op <|"   uterm
+primrec
   subst_Var      "(Var v <| s) = assoc v (Var v) s"
   subst_Const  "(Const c <| s) = Const c"
   subst_Comb  "(Comb M N <| s) = Comb (M <| s) (N <| s)"
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/UTerm.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -7,7 +7,7 @@
 Binary trees with leaves that are constants or variables.
 *)
 
-UTerm = Finite + 
+UTerm = Finite + Datatype +
 
 datatype 'a uterm = Var ('a) 
                   | Const ('a)
@@ -19,20 +19,20 @@
 uterm_size ::  'a uterm => nat
 
 
-primrec vars_of   uterm
-vars_of_Var   "vars_of (Var v) = {v}"
-vars_of_Const "vars_of (Const c) = {}"
-vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
+primrec
+  vars_of_Var   "vars_of (Var v) = {v}"
+  vars_of_Const "vars_of (Const c) = {}"
+  vars_of_Comb  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
 
-primrec "op <:"   uterm
-occs_Var   "u <: (Var v) = False"
-occs_Const "u <: (Const c) = False"
-occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
+primrec
+  occs_Var   "u <: (Var v) = False"
+  occs_Const "u <: (Const c) = False"
+  occs_Comb  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
 
-primrec uterm_size  uterm
-uterm_size_Var   "uterm_size (Var v) = 0"
-uterm_size_Const "uterm_size (Const c) = 0"
-uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
+primrec
+  uterm_size_Var   "uterm_size (Var v) = 0"
+  uterm_size_Const "uterm_size (Const c) = 0"
+  uterm_size_Comb  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
 
 end
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/Subst/Unify.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -160,7 +160,7 @@
 			inv_image_def, less_eq]) 1);
 (** LEVEL 7 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [option.split]) 1);
 by (strip_tac 1);
 by (rtac (trans_unifyRel RS transD) 1);
 by (Blast_tac 1);
@@ -183,7 +183,7 @@
 \                            of None => None    \
 \                             | Some sigma => Some (theta <> sigma)))";
 by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
-			   addsplits [split_option_case]) 1);
+			   addsplits [option.split]) 1);
 qed "unifyCombComb";
 
 
@@ -219,7 +219,7 @@
 by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
 (** LEVEL 8 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
+by (asm_simp_tac (simpset() addsplits [option.split]) 1);
 by (strip_tac 1);
 by (rotate_tac ~2 1);
 by (asm_full_simp_tac 
@@ -244,7 +244,7 @@
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
 by (ALLGOALS 
     (asm_simp_tac 
-       (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
+       (simpset() addsimps [Var_Idem] addsplits [option.split])));
 (*Comb-Comb case*)
 by Safe_tac;
 by (REPEAT (dtac spec 1 THEN mp_tac 1));
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/TLA/Inc/Pcount.thy
--- a/src/HOL/TLA/Inc/Pcount.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Inc/Pcount.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
 and case distinction tactics.
 *)
 
-Pcount  =  HOL + Arith +
+Pcount  =  Datatype +
 
 datatype pcount = a | b | g
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/TLA/Memory/MIParameters.thy
--- a/src/HOL/TLA/Memory/MIParameters.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/MIParameters.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -9,7 +9,7 @@
     RPC-Memory example: Parameters of the memory implementation.
 *)
 
-MIParameters = Arith +
+MIParameters = Datatype +
 
 datatype  histState  =  histA | histB
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/TLA/Memory/Memory.ML
--- a/src/HOL/TLA/Memory/Memory.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/Memory.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -148,13 +148,13 @@
 	     res_inst_tac [("s","arg(ch s p)")] sumE 1,
 	      action_simp_tac (simpset()addsimps[Read_def,enabled_ex,base_pair])
 	                      [action_mp ReadInner_enabled,exI] [] 1,
-	      split_all_tac 1, rename_tac "a b" 1, Rd.induct_tac "a" 1,
+	      split_all_tac 1, rename_tac "a b" 1, induct_tac "a" 1,
 	     (* introduce a trivial subgoal to solve flex-flex constraint?! *)
 	      subgoal_tac "b = snd(a,b)" 1,
 	       TRYALL Simp_tac,  (* solves "read" case *)
 	     etac swap 1,
 	     action_simp_tac (simpset()addsimps[Write_def,enabled_ex,base_pair])
 	                     [action_mp WriteInner_enabled,exI] [] 1,
-	     split_all_tac 1, rename_tac "a aa b" 1, Wr.induct_tac "a" 1,
+	     split_all_tac 1, rename_tac "a aa b" 1, induct_tac "a" 1,
 	     subgoal_tac "(aa = fst(snd(a,aa,b))) & (b = snd(snd(a,aa,b)))" 1,
 	     ALLGOALS Simp_tac ]);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/TLA/Memory/MemoryParameters.thy
--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -9,7 +9,7 @@
     RPC-Memory example: Memory parameters
 *)
 
-MemoryParameters = Prod + Sum + Arith + RPCMemoryParams +
+MemoryParameters = Datatype + RPCMemoryParams +
 
 (* the memory operations. nb: data types must be defined in theories
    that do not include Intensional -- otherwise the induction rule
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/I.ML
--- a/src/HOL/W0/I.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/I.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -12,7 +12,7 @@
   "! a m s s' t n.  \
 \    (new_tv m a & new_tv m s) --> I e a m s = Ok(s',t,n) -->   \
 \    ( ? r. W e ($ s a) m = Ok(r, $ s' t, n) & s' = ($ r o s) )";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 
   (* case Var n *)
   by (simp_tac (simpset() addsimps [app_subst_list]
@@ -143,7 +143,7 @@
 
 Goal "!a m s. \
 \  new_tv m a & new_tv m s --> I e a m s = Fail --> W e ($s a) m = Fail";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
   by (simp_tac (simpset() addsimps [app_subst_list]) 1);
  by (Simp_tac 1);
  by (strip_tac 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/I.thy
--- a/src/HOL/W0/I.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/I.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
 consts
         I :: [expr, typ list, nat, subst] => result_W
 
-primrec I expr
+primrec
         "I (Var i) a n s = (if i < length a then Ok(s, a!i, n)
                                     else Fail)"
         "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/Type.ML
--- a/src/HOL/W0/Type.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/Type.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -17,7 +17,7 @@
 Goalw [id_subst_def]
   "$ id_subst = (%t::typ. t)";
 by (rtac ext 1);
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_te";
 Addsimps [app_subst_id_te];
@@ -26,7 +26,7 @@
 Goalw [app_subst_list]
   "$ id_subst = (%ts::typ list. ts)";
 by (rtac ext 1); 
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "app_subst_id_tel";
 Addsimps [app_subst_id_tel];
@@ -69,13 +69,13 @@
 (* composition of substitutions *)
 Goal
   "$ g ($ f t::typ) = $ (%x. $ g (f x) ) t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_comp_te";
 
 Goalw [app_subst_list]
   "$ g ($ f ts::typ list) = $ (%x. $ g (f x)) ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -149,21 +149,21 @@
 Goal 
   "new_tv n  = list_all (new_tv n)";
 by (rtac ext 1);
-by (list.induct_tac "x" 1);
+by (induct_tac "x" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "new_tv_list";
 
 (* substitution affects only variables occurring freely *)
 Goal
   "new_tv n (t::typ) --> $(%x. if x=n then t' else s x) t = $s t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "subst_te_new_tv";
 Addsimps [subst_te_new_tv];
 
 Goal
   "new_tv n (ts::typ list) --> $(%x. if x=n then t else s x) ts = $s ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "subst_tel_new_tv";
 Addsimps [subst_tel_new_tv];
@@ -171,7 +171,7 @@
 (* all greater variables are also new *)
 Goal
   "n<=m --> new_tv n (t::typ) --> new_tv m t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addIs [less_le_trans] addss simpset()) 1);
 (* case Fun t1 t2 *)
@@ -181,7 +181,7 @@
 
 Goal 
   "n<=m --> new_tv n (ts::typ list) --> new_tv m ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
@@ -209,7 +209,7 @@
 
 Goal
   "new_tv n s --> new_tv n (t::typ) --> new_tv n ($ s t)";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_te";
 Addsimps [new_tv_subst_te];
@@ -217,7 +217,7 @@
 Goal
   "new_tv n s --> new_tv n (ts::typ list) --> new_tv n ($ s ts)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 by (ALLGOALS(fast_tac (HOL_cs addss (simpset() addsimps [new_tv_subst]))));
 qed_spec_mp "new_tv_subst_tel";
 Addsimps [new_tv_subst_tel];
@@ -226,7 +226,7 @@
 Goal
   "new_tv n ts --> new_tv (Suc n) ((TVar n)#ts)";
 by (simp_tac (simpset() addsimps [new_tv_list]) 1);
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 by (ALLGOALS Asm_full_simp_tac);
 qed "new_tv_Suc_list";
 
@@ -255,7 +255,7 @@
 
 Goal
   "(t::typ) mem ts --> free_tv t <= free_tv ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case x#xl *)
@@ -269,7 +269,7 @@
    occurring in the type structure *)
 Goal
   "$ s1 (t::typ) = $ s2 t --> n:(free_tv t) --> s1 n = s2 n";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Fun t1 t2 *)
@@ -278,7 +278,7 @@
 
 Goal
   "(!n. n:(free_tv t) --> s1 n = s2 n) --> $ s1 (t::typ) = $ s2 t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Fun t1 t2 *)
@@ -286,7 +286,7 @@
 qed_spec_mp "eq_free_eq_subst_te";
 
 Goal "$s1 (ts::typ list) = $s2 ts --> n:(free_tv ts) --> s1 n = s2 n";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
@@ -294,7 +294,7 @@
 qed_spec_mp "eq_subst_tel_eq_free";
 
 Goal "(!n. n:(free_tv ts) --> s1 n = s2 n) --> $s1 (ts::typ list) = $s2 ts";
-by (list.induct_tac "ts" 1); 
+by (induct_tac "ts" 1); 
 (* case [] *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case x#xl *)
@@ -323,7 +323,7 @@
 qed "free_tv_subst_var";
 
 Goal "free_tv ($ s (t::typ)) <= cod s Un free_tv t";
-by (typ.induct_tac "t" 1);
+by (induct_tac "t" 1);
 (* case TVar n *)
 by (simp_tac (simpset() addsimps [free_tv_subst_var]) 1);
 (* case Fun t1 t2 *)
@@ -331,7 +331,7 @@
 qed "free_tv_app_subst_te";     
 
 Goal "free_tv ($ s (ts::typ list)) <= cod s Un free_tv ts";
-by (list.induct_tac "ts" 1);
+by (induct_tac "ts" 1);
 (* case [] *)
 by (Simp_tac 1);
 (* case a#al *)
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/Type.thy
--- a/src/HOL/W0/Type.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/Type.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -36,7 +36,7 @@
 consts
         app_subst :: [subst, 'a::type_struct] => 'a::type_struct ("$")
 
-primrec app_subst typ
+primrec
   app_subst_TVar  "$ s (TVar n) = s n" 
   app_subst_Fun   "$ s (t1 -> t2) = ($ s t1) -> ($ s t2)" 
 
@@ -47,11 +47,11 @@
 consts
         free_tv :: ['a::type_struct] => nat set
 
-primrec free_tv typ
+primrec
   "free_tv (TVar m) = {m}"
   "free_tv (t1 -> t2) = (free_tv t1) Un (free_tv t2)"
 
-primrec free_tv List.list
+primrec
   "free_tv [] = {}"
   "free_tv (x#l) = (free_tv x) Un (free_tv l)"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/W.ML
--- a/src/HOL/W0/W.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/W.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
 
 (* correctness of W with respect to has_type *)
 Goal "!a s t m n . Ok (s,t,m) = W e a n --> $s a |- e :: t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (Asm_simp_tac 1);
 (* case Abs e *)
@@ -41,7 +41,7 @@
 
 (* the resulting type variable is always greater or equal than the given one *)
 Goal "!a n s t m. W e a n  = Ok (s,t,m) --> n<=m";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var(n) *)
 by (fast_tac (HOL_cs addss simpset()) 1);
 (* case Abs e *)
@@ -85,7 +85,7 @@
 Goal
      "!n a s t m. new_tv n a --> W e a n = Ok (s,t,m) -->    \
 \                 new_tv m s & new_tv m t";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addDs [list_all_nth] addss (simpset() 
         addsimps [id_subst_def,new_tv_list,new_tv_subst])) 1);
@@ -151,7 +151,7 @@
 
 Goal "!n a s t m v. W e a n = Ok (s,t,m) -->            \
 \         (v:free_tv s | v:free_tv t) --> v<n --> v:free_tv a";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (fast_tac (HOL_cs addIs [nth_mem,subsetD,ftv_mem_sub_ftv_list] 
     addss simpset()) 1);
@@ -217,7 +217,7 @@
  "!s' a t' n. $s' a |- e :: t' --> new_tv n a -->     \
 \             (? s t. (? m. W e a n = Ok (s,t,m)) &  \
 \                     (? r. $s' a = $r ($s a) & t' = $r t))";
-by (expr.induct_tac "e" 1);
+by (induct_tac "e" 1);
 (* case Var n *)
 by (strip_tac 1);
 by (simp_tac (simpset() addcongs [conj_cong]) 1);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/W0/W.thy
--- a/src/HOL/W0/W.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/W0/W.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -15,7 +15,7 @@
 consts
         W :: [expr, typ list, nat] => result_W
 
-primrec W expr
+primrec
   "W (Var i) a n = (if i < length a then Ok(id_subst, a!i, n)
                     else Fail)"
   "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/BT.ML
--- a/src/HOL/ex/BT.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/BT.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -11,48 +11,48 @@
 (** BT simplification **)
 
 Goal "n_leaves(reflect(t)) = n_leaves(t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
 qed "n_leaves_reflect";
 
 Goal "n_nodes(reflect(t)) = n_nodes(t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_commute])));
 qed "n_nodes_reflect";
 
 (*The famous relationship between the numbers of leaves and nodes*)
 Goal "n_leaves(t) = Suc(n_nodes(t))";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "n_leaves_nodes";
 
 Goal "reflect(reflect(t))=t";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "reflect_reflect_ident";
 
 Goal "bt_map f (reflect t) = reflect (bt_map f t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "bt_map_reflect";
 
 Goal "inorder (bt_map f t) = map f (inorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "inorder_bt_map";
 
 Goal "preorder (reflect t) = rev (postorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "preorder_reflect";
 
 Goal "inorder (reflect t) = rev (inorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "inorder_reflect";
 
 Goal "postorder (reflect t) = rev (preorder t)";
-by (bt.induct_tac "t" 1);
+by (induct_tac "t" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "postorder_reflect";
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/BT.thy
--- a/src/HOL/ex/BT.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/BT.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -19,31 +19,31 @@
     inorder     :: 'a bt => 'a list
     postorder   :: 'a bt => 'a list
 
-primrec n_nodes bt
+primrec
   "n_nodes (Lf) = 0"
   "n_nodes (Br a t1 t2) = Suc(n_nodes t1 + n_nodes t2)"
 
-primrec n_leaves bt
+primrec
   "n_leaves (Lf) = Suc 0"
   "n_leaves (Br a t1 t2) = n_leaves t1 + n_leaves t2"
 
-primrec reflect bt
+primrec
   "reflect (Lf) = Lf"
   "reflect (Br a t1 t2) = Br a (reflect t2) (reflect t1)"
 
-primrec bt_map bt
+primrec
   "bt_map f Lf = Lf"
   "bt_map f (Br a t1 t2) = Br (f a) (bt_map f t1) (bt_map f t2)"
 
-primrec preorder bt
+primrec
   "preorder (Lf) = []"
   "preorder (Br a t1 t2) = [a] @ (preorder t1) @ (preorder t2)"
 
-primrec inorder bt
+primrec
   "inorder (Lf) = []"
   "inorder (Br a t1 t2) = (inorder t1) @ [a] @ (inorder t2)"
 
-primrec postorder bt
+primrec
   "postorder (Lf) = []"
   "postorder (Br a t1 t2) = (postorder t1) @ (postorder t2) @ [a]"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/InSort.ML
--- a/src/HOL/ex/InSort.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/InSort.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -7,13 +7,13 @@
 *)
 
 Goal "!y. mset(ins f x xs) y = mset (x#xs) y";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "mset_ins";
 Addsimps [mset_ins];
 
 Goal "!x. mset(insort f xs) x = mset xs x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "insort_permutes";
 
@@ -25,7 +25,7 @@
 
 val prems = goalw InSort.thy [total_def,transf_def]
   "[| total(f); transf(f) |] ==>  sorted f (ins f x xs) = sorted f xs";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
@@ -33,6 +33,6 @@
 Addsimps [sorted_ins];
 
 Goal "[| total(f); transf(f) |] ==>  sorted f (insort f xs)";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sorted_insort";
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/InSort.thy
--- a/src/HOL/ex/InSort.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/InSort.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -12,10 +12,10 @@
   ins :: [['a,'a]=>bool, 'a, 'a list] => 'a list
   insort :: [['a,'a]=>bool, 'a list] => 'a list
 
-primrec ins List.list
+primrec
   "ins f x [] = [x]"
   "ins f x (y#ys) = (if f x y then (x#y#ys) else y#(ins f x ys))"
-primrec insort List.list
+primrec
   "insort f [] = []"
   "insort f (x#xs) = ins f x (insort f xs)"
 end
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/NatSum.thy
--- a/src/HOL/ex/NatSum.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/NatSum.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -8,7 +8,7 @@
 
 NatSum = Arith +
 consts sum     :: [nat=>nat, nat] => nat
-primrec "sum" nat 
+primrec 
   "sum f 0 = 0"
   "sum f (Suc n) = f(n) + sum f n"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Primes.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -11,7 +11,7 @@
 	Isabelle prove those conditions.
 *)
 
-Primes = Divides + WF_Rel +
+Primes = Divides + Recdef + Datatype +
 consts
   is_gcd  :: [nat,nat,nat]=>bool          (*gcd as a relation*)
   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/Primrec.thy
--- a/src/HOL/ex/Primrec.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Primrec.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -25,12 +25,12 @@
     "ack (Suc m, Suc n) = ack (m, ack (Suc m, n))"
 
 consts  list_add :: nat list => nat
-primrec list_add list
+primrec
   "list_add []     = 0"
   "list_add (m#ms) = m + list_add ms"
 
 consts  zeroHd  :: nat list => nat
-primrec zeroHd list
+primrec
   "zeroHd []     = 0"
   "zeroHd (m#ms) = m"
 
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/Qsort.ML
--- a/src/HOL/ex/Qsort.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Qsort.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -36,7 +36,7 @@
 
 goal List.thy
   "(!x:set[x:xs. P(x)].Q(x)) = (!x:set xs. P(x)-->Q(x))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed"Ball_set_filter";
 Addsimps [Ball_set_filter];
@@ -44,7 +44,7 @@
 Goal
  "sorted le (xs@ys) = (sorted le xs & sorted le ys & \
 \                     (!x:set xs. !y:set ys. le x y))";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "sorted_append";
 Addsimps [sorted_append];
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/Sorting.ML
--- a/src/HOL/ex/Sorting.ML	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Sorting.ML	Fri Jul 24 13:19:38 1998 +0200
@@ -7,20 +7,20 @@
 *)
 
 Goal "!x. mset (xs@ys) x = mset xs x + mset ys x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "mset_append";
 
 Goal "!x. mset [x:xs. ~p(x)] x + mset [x:xs. p(x)] x = \
 \                     mset xs x";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "mset_compl_add";
 
 Addsimps [mset_append, mset_compl_add];
 
 Goal "set xs = {x. mset xs x ~= 0}";
-by (list.induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 by (Fast_tac 1);
 qed "set_via_mset";
@@ -29,8 +29,8 @@
 
 val prems = goalw Sorting.thy [transf_def]
   "transf(le) ==> sorted1 le xs = sorted le xs";
-by (list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac (simpset() addsplits [split_list_case])));
+by (induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [list.split])));
 by (cut_facts_tac prems 1);
 by (Fast_tac 1);
 qed "sorted1_is_sorted";
diff -r 89f162de39cf -r 9b8547a9496a src/HOL/ex/Sorting.thy
--- a/src/HOL/ex/Sorting.thy	Fri Jul 24 13:03:20 1998 +0200
+++ b/src/HOL/ex/Sorting.thy	Fri Jul 24 13:19:38 1998 +0200
@@ -14,16 +14,16 @@
   total  :: (['a,'a] => bool) => bool
   transf :: (['a,'a] => bool) => bool
 
-primrec sorted1 list
+primrec
   "sorted1 le [] = True"
   "sorted1 le (x#xs) = ((case xs of [] => True | y#ys => le x y) &
                         sorted1 le xs)"
 
-primrec sorted list
+primrec
   "sorted le [] = True"
   "sorted le (x#xs) = ((!y:set xs. le x y) & sorted le xs)"
 
-primrec mset list
+primrec
   "mset [] y = 0"
   "mset (x#xs) y = (if x=y then Suc(mset xs y) else mset xs y)"