src/HOL/Lex/Prefix.ML

 qed "prefix_prefix";
 Addsimps [prefix_prefix];
 
 Goalw [prefix_def]
    "(xs <= y#ys) = (xs=[] | (? zs. xs=y#zs & zs <= ys))";
-by (exhaust_tac "xs" 1);
+by (cases_tac "xs" 1);
 by Auto_tac;
 qed "prefix_Cons";
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
 by (res_inst_tac [("xs","zs")] rev_induct 1);

 qed "prefix_append";
 
 Goalw [prefix_def]
   "[| xs <= ys; length xs < length ys |] ==> xs @ [ys ! length xs] <= ys";
 by (auto_tac(claset(), simpset() addsimps [nth_append]));
-by (exhaust_tac "ys" 1);
+by (cases_tac "ys" 1);
 by Auto_tac;
 qed "append_one_prefix";
 
 Goalw [prefix_def] "xs <= ys ==> length xs <= length ys";
 by Auto_tac;