src/HOL/Subst/Unify.ML
changeset 3919 c036caebfc75
parent 3724 f33e301a89f5
child 4071 4747aefbbc52
     1.1 --- a/src/HOL/Subst/Unify.ML	Fri Oct 17 15:23:14 1997 +0200
     1.2 +++ b/src/HOL/Subst/Unify.ML	Fri Oct 17 15:25:12 1997 +0200
     1.3 @@ -154,14 +154,14 @@
     1.4  by (res_inst_tac [("u","M1"),("v","M2")] unifyInduct0 1);
     1.5  by (ALLGOALS 
     1.6      (asm_simp_tac (!simpset addsimps (var_elimR::unifyRules0)
     1.7 -			    setloop (split_tac [expand_if]))));
     1.8 +			    addsplits [expand_if])));
     1.9  (*Const-Const case*)
    1.10  by (simp_tac
    1.11      (!simpset addsimps [unifyRel_def, lex_prod_def, measure_def,
    1.12  			inv_image_def, less_eq]) 1);
    1.13  (** LEVEL 7 **)
    1.14  (*Comb-Comb case*)
    1.15 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
    1.16 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
    1.17  by (strip_tac 1);
    1.18  by (rtac (trans_unifyRel RS transD) 1);
    1.19  by (Blast_tac 1);
    1.20 @@ -184,7 +184,7 @@
    1.21  \                            of None => None    \
    1.22  \                             | Some sigma => Some (theta <> sigma)))";
    1.23  by (asm_simp_tac (!simpset addsimps (unify_TC::unifyRules0)
    1.24 -			   setloop split_tac [expand_option_case]) 1);
    1.25 +			   addsplits [expand_option_case]) 1);
    1.26  qed "unifyCombComb";
    1.27  
    1.28  
    1.29 @@ -207,7 +207,7 @@
    1.30  
    1.31  goal Unify.thy "!theta. unify(M,N) = Some theta --> MGUnifier theta M N";
    1.32  by (res_inst_tac [("u","M"),("v","N")] unifyInduct 1);
    1.33 -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if])));
    1.34 +by (ALLGOALS (asm_simp_tac (!simpset addsplits [expand_if])));
    1.35  (*Const-Const case*)
    1.36  by (simp_tac (!simpset addsimps [MGUnifier_def,Unifier_def]) 1);
    1.37  (*Const-Var case*)
    1.38 @@ -220,7 +220,7 @@
    1.39  by (simp_tac (!simpset addsimps [MGUnifier_Var]) 1);
    1.40  (** LEVEL 8 **)
    1.41  (*Comb-Comb case*)
    1.42 -by (asm_simp_tac (!simpset setloop split_tac [expand_option_case]) 1);
    1.43 +by (asm_simp_tac (!simpset addsplits [expand_option_case]) 1);
    1.44  by (strip_tac 1);
    1.45  by (rotate_tac ~2 1);
    1.46  by (asm_full_simp_tac 
    1.47 @@ -246,7 +246,7 @@
    1.48  by (ALLGOALS 
    1.49      (asm_simp_tac 
    1.50         (!simpset addsimps [Var_Idem] 
    1.51 -	         setloop split_tac[expand_if, expand_option_case])));
    1.52 +	         addsplits [expand_if,expand_option_case])));
    1.53  (*Comb-Comb case*)
    1.54  by (safe_tac (!claset));
    1.55  by (REPEAT (dtac spec 1 THEN mp_tac 1));