src/HOL/Subst/Unify.ML
changeset 5184 9b8547a9496a
parent 5119 58d267fc8630
child 5278 a903b66822e2
     1.1 --- a/src/HOL/Subst/Unify.ML	Fri Jul 24 13:03:20 1998 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Fri Jul 24 13:19:38 1998 +0200
     1.3 @@ -160,7 +160,7 @@
     1.4  			inv_image_def, less_eq]) 1);
     1.5  (** LEVEL 7 **)
     1.6  (*Comb-Comb case*)
     1.7 -by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
     1.8 +by (asm_simp_tac (simpset() addsplits [option.split]) 1);
     1.9  by (strip_tac 1);
    1.10  by (rtac (trans_unifyRel RS transD) 1);
    1.11  by (Blast_tac 1);
    1.12 @@ -183,7 +183,7 @@
    1.13  \                            of None => None    \
    1.14  \                             | Some sigma => Some (theta <> sigma)))";
    1.15  by (asm_simp_tac (simpset() addsimps (unify_TC::unifyRules0)
    1.16 -			   addsplits [split_option_case]) 1);
    1.17 +			   addsplits [option.split]) 1);
    1.18  qed "unifyCombComb";
    1.19  
    1.20  
    1.21 @@ -219,7 +219,7 @@
    1.22  by (simp_tac (simpset() addsimps [MGUnifier_Var]) 1);
    1.23  (** LEVEL 8 **)
    1.24  (*Comb-Comb case*)
    1.25 -by (asm_simp_tac (simpset() addsplits [split_option_case]) 1);
    1.26 +by (asm_simp_tac (simpset() addsplits [option.split]) 1);
    1.27  by (strip_tac 1);
    1.28  by (rotate_tac ~2 1);
    1.29  by (asm_full_simp_tac 
    1.30 @@ -244,7 +244,7 @@
    1.31  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.32  by (ALLGOALS 
    1.33      (asm_simp_tac 
    1.34 -       (simpset() addsimps [Var_Idem] addsplits [split_option_case])));
    1.35 +       (simpset() addsimps [Var_Idem] addsplits [option.split])));
    1.36  (*Comb-Comb case*)
    1.37  by Safe_tac;
    1.38  by (REPEAT (dtac spec 1 THEN mp_tac 1));