--- a/src/HOL/Tools/sat_funcs.ML Mon Jul 27 17:36:30 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Mon Jul 27 20:45:40 2009 +0200
@@ -410,7 +410,7 @@
(* or "True" *)
(* ------------------------------------------------------------------------- *)
-fun rawsat_tac i = METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
+fun rawsat_tac i = OldGoals.METAHYPS (fn prems => rtac (rawsat_thm (map cprop_of prems)) 1) i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)