src/HOL/Subst/Unify.ML
changeset 4071 4747aefbbc52
parent 3919 c036caebfc75
child 4089 96fba19bcbe2
     1.1 --- a/src/HOL/Subst/Unify.ML	Mon Nov 03 08:16:35 1997 +0100
     1.2 +++ b/src/HOL/Subst/Unify.ML	Mon Nov 03 09:57:35 1997 +0100
     1.3 @@ -161,7 +161,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 [expand_option_case]) 1);
     1.8 +by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
     1.9  by (strip_tac 1);
    1.10  by (rtac (trans_unifyRel RS transD) 1);
    1.11  by (Blast_tac 1);
    1.12 @@ -184,7 +184,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 [expand_option_case]) 1);
    1.17 +			   addsplits [split_option_case]) 1);
    1.18  qed "unifyCombComb";
    1.19  
    1.20  
    1.21 @@ -220,7 +220,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 [expand_option_case]) 1);
    1.26 +by (asm_simp_tac (!simpset addsplits [split_option_case]) 1);
    1.27  by (strip_tac 1);
    1.28  by (rotate_tac ~2 1);
    1.29  by (asm_full_simp_tac 
    1.30 @@ -246,7 +246,7 @@
    1.31  by (ALLGOALS 
    1.32      (asm_simp_tac 
    1.33         (!simpset addsimps [Var_Idem] 
    1.34 -	         addsplits [expand_if,expand_option_case])));
    1.35 +	         addsplits [expand_if,split_option_case])));
    1.36  (*Comb-Comb case*)
    1.37  by (safe_tac (!claset));
    1.38  by (REPEAT (dtac spec 1 THEN mp_tac 1));