1.1 --- a/src/HOL/IMPP/Misc.ML	Tue Mar 28 12:28:24 2000 +0200
     1.2 +++ b/src/HOL/IMPP/Misc.ML	Tue Mar 28 17:31:36 2000 +0200
     1.3 @@ -13,8 +13,6 @@
     1.4  Goalw [update_def] "s[Loc Y::=s<Y>] = s";
     1.5  by (induct_tac "s" 1);
     1.6  by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
     1.7 -br ext 1;
     1.8 -by (Simp_tac 1);
     1.9  qed "update_Loc_idem2";
    1.10  Addsimps[update_Loc_idem2];
    1.11