src/HOL/Subst/Unify.ML

 by (simp_tac
     (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
 			inv_image_def, less_eq]) 1);
 (** LEVEL 7 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
 by (strip_tac 1);
 by (rtac (trans_unifyRel RS transD) 1);
 by (Blast_tac 1);
 by (simp_tac (HOL_ss addsimps [subst_Comb RS sym]) 1);
 by (rtac Rassoc 1);

 \        of None => None                \
 \         | Some theta => (case unify(N1 <| theta, N2 <| theta)        \
 \                            of None => None    \
 \                             | Some sigma => Some (theta <> sigma)))";
 by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
-			   addsplits [expand_option_case]) 1);
+			   addsplits [split_option_case]) 1);
 qed "unifyCombComb";
 
 
 val unifyRules = rev (unifyCombComb :: tl (rev unifyRules0));
 

 (*Comb-Var case*)
 by (stac mgu_sym 1);
 by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
 (** LEVEL 8 **)
 (*Comb-Comb case*)
-by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
+by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
 by (strip_tac 1);
 by (rotate_tac ~2 1);
 by (asm_full_simp_tac 
     (!simpset addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
 by (safe_tac (!claset) THEN rename_tac "theta sigma gamma" 1);

 goal Unify.thy "!theta. unify(M,N) = Some theta --> Idem theta";
 by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
 by (ALLGOALS 
     (asm_simp_tac 
        (!simpset addsimps [Var_Idem] 
-	         addsplits [expand_if,expand_option_case])));
+	         addsplits [expand_if,split_option_case])));
 (*Comb-Comb case*)
 by (safe_tac (!claset));
 by (REPEAT (dtac spec 1 THEN mp_tac 1));
 by (safe_tac (!claset addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
 by (rtac Idem_comp 1);