src/HOL/Subst/Unify.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4686 74a12e86b20b
     1.1 --- a/src/HOL/Subst/Unify.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Subst/Unify.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -225,7 +225,7 @@
     1.4  by (rotate_tac ~2 1);
     1.5  by (asm_full_simp_tac 
     1.6      (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
     1.7 -by (safe_tac (claset()) THEN rename_tac "theta sigma gamma" 1);
     1.8 +by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
     1.9  by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
    1.10  by (etac exE 1 THEN rename_tac "delta" 1);
    1.11  by (eres_inst_tac [("x","delta")] allE 1);
    1.12 @@ -248,7 +248,7 @@
    1.13         (simpset() addsimps [Var_Idem] 
    1.14  	         addsplits [expand_if,split_option_case])));
    1.15  (*Comb-Comb case*)
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  by (REPEAT (dtac spec 1 THEN mp_tac 1));
    1.19  by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
    1.20  by (rtac Idem_comp 1);