--- a/src/Provers/blast.ML Sun Oct 14 20:02:59 2001 +0200
+++ b/src/Provers/blast.ML Sun Oct 14 20:04:05 2001 +0200
@@ -67,7 +67,6 @@
uwrappers: (string * wrapper) list,
safe0_netpair: netpair, safep_netpair: netpair,
haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
- val atomize: thm list
val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
end;
@@ -117,7 +116,6 @@
struct
type claset = Data.claset;
-val atomize_goal = Method.atomize_goal Data.atomize;
val trace = ref false
and stats = ref false; (*for runtime and search statistics*)
@@ -1277,7 +1275,7 @@
"lim" is depth limit.*)
fun timing_depth_tac start cs lim i st0 =
(initialize();
- let val st = atomize_goal i st0;
+ let val st = ObjectLogic.atomize_goal i st0;
val {sign,...} = rep_thm st
val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
val hyps = strip_imp_prems skoprem