changeset 10906 | de95ba2760fe |
parent 10429 | 8820f787e61e |
child 11748 | 06eb315831ff |
--- a/src/FOL/blastdata.ML Tue Jan 16 00:27:37 2001 +0100 +++ b/src/FOL/blastdata.ML Tue Jan 16 00:28:50 2001 +0100 @@ -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 = thms "atomize'" + val atomize = atomize_rules val cla_modifiers = Cla.cla_modifiers; val cla_meth' = Cla.cla_meth' end;