src/HOL/ex/meson.ML
changeset 1820 e381e1c51689
parent 1764 69b93ffc29ec
child 2031 03a843f0f447
--- 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));