author | wenzelm |
Wed, 09 Aug 2000 20:43:03 +0200 | |
changeset 9561 | 714ad541a133 |
parent 9560 | b87a6afe5881 |
child 9562 | 6b07b56aa3a8 |
--- a/src/FOL/blastdata.ML Wed Aug 09 17:10:41 2000 +0200 +++ b/src/FOL/blastdata.ML Wed Aug 09 20:43:03 2000 +0200 @@ -10,7 +10,7 @@ val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac val claset = Cla.claset val rep_cs = Cla.rep_cs - val atomize = [thm "all_eq", thm "imp_eq"] + val atomize = thms "atomize" val cla_modifiers = Cla.cla_modifiers; val cla_meth' = Cla.cla_meth' end;