src/HOL/Auth/OtwayRees.ML
changeset 3207 fe79ad367d77
parent 3121 cbb6c0c1c58a
child 3451 d10f100676d8
     1.1 --- a/src/HOL/Auth/OtwayRees.ML	Thu May 15 15:51:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees.ML	Thu May 15 15:51:47 1997 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4        (!claset addIs [impOfSubs analz_subset_parts]
     1.5                 addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
     1.6                        impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
     1.7 -               unsafe_addss (!simpset)) 1);
     1.8 +               addss (!simpset)) 1);
     1.9  by (ALLGOALS Blast_tac);
    1.10  qed_spec_mp "new_keys_not_used";
    1.11