--- a/src/HOL/ex/meson.ML Fri Jun 21 11:57:00 1996 +0200
+++ b/src/HOL/ex/meson.ML Fri Jun 21 12:18:50 1996 +0200
@@ -16,7 +16,7 @@
(*Prove theorems using fast_tac*)
fun prove_fun s =
prove_goal HOL.thy s
- (fn prems => [ cut_facts_tac prems 1, fast_tac HOL_cs 1 ]);
+ (fn prems => [ cut_facts_tac prems 1, Fast_tac 1 ]);
(**** Negation Normal Form ****)
@@ -63,7 +63,7 @@
val [major] = goal HOL.thy
"! x. ? y. Q x y ==> ? f. ! x. Q x (f x)";
by (cut_facts_tac [major] 1);
-by (fast_tac (HOL_cs addEs [selectI]) 1);
+by (fast_tac (!claset addEs [selectI]) 1);
qed "choice";
@@ -430,7 +430,7 @@
(*First, breaks the goal into independent units*)
val safe_best_meson_tac =
- SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+ SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (best_meson_tac size_of_subgoals));
(** Depth-first search version **)
@@ -464,7 +464,7 @@
(prolog_step_tac' (make_horns cls))));
val safe_meson_tac =
- SELECT_GOAL (TRY (safe_tac HOL_cs) THEN
+ SELECT_GOAL (TRY (safe_tac (!claset)) THEN
TRYALL (iter_deepen_meson_tac));