--- a/src/FOL/blastdata.ML Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/blastdata.ML Fri Nov 10 19:00:22 2000 +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 = thms "atomize'"
val cla_modifiers = Cla.cla_modifiers;
val cla_meth' = Cla.cla_meth'
end;
--- a/src/FOL/cladata.ML Fri Nov 10 16:31:28 2000 +0100
+++ b/src/FOL/cladata.ML Fri Nov 10 19:00:22 2000 +0100
@@ -24,7 +24,7 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
- val atomize = thms "atomize"
+ val atomize = thms "atomize'"
end;
structure Cla = ClassicalFun(Classical_Data);
--- a/src/HOL/blastdata.ML Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/blastdata.ML Fri Nov 10 19:00:22 2000 +0100
@@ -23,7 +23,7 @@
val hyp_subst_tac = Hypsubst.blast_hyp_subst_tac
val claset = Classical.claset
val rep_cs = Classical.rep_cs
- val atomize = thms "atomize"
+ val atomize = thms "atomize'"
val cla_modifiers = Classical.cla_modifiers;
val cla_meth' = Classical.cla_meth'
end;
--- a/src/HOL/cladata.ML Fri Nov 10 16:31:28 2000 +0100
+++ b/src/HOL/cladata.ML Fri Nov 10 19:00:22 2000 +0100
@@ -47,7 +47,7 @@
val classical = classical
val sizef = size_of_thm
val hyp_subst_tacs=[hyp_subst_tac]
- val atomize = thms "atomize"
+ val atomize = thms "atomize'"
end;
structure Classical = ClassicalFun(Classical_Data);