--- 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));