src/HOL/Auth/OtwayRees_AN.ML
changeset 3207 fe79ad367d77
parent 3121 cbb6c0c1c58a
child 3451 d10f100676d8
     1.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Thu May 15 15:51:09 1997 +0200
     1.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Thu May 15 15:51:47 1997 +0200
     1.3 @@ -119,7 +119,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  (*OR3*)
    1.10  by (Blast_tac 1);
    1.11  qed_spec_mp "new_keys_not_used";