src/HOL/ex/meson.ML

 writeln"File HOL/ex/meson.";
 
 (*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 ****)
 
 (*** de Morgan laws ***)
 

 
 (*"Axiom" of Choice, proved using the description operator*)
 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";
 
 
 (***** Generating clauses for the Meson Proof Procedure *****)
 

                          (has_fewer_prems 1, sizef)
 			 (prolog_step_tac (make_horns cls) 1));
 
 (*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 **)
 
 val depth_meson_tac =

          (THEN_ITER_DEEPEN (resolve_tac (gocls cls) 1)
 	                   (has_fewer_prems 1)
 	                   (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));
 
 
 writeln"Reached end of file.";