src/HOL/Tools/sat_funcs.ML

 (*        [| c1; c2; ...; ck |] ==> False                                    *)
 (*      where each cj is a non-empty clause (i.e. a disjunction of literals) *)
 (*      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                                    *)
 (*        [| A1 ; ... ; An |] ==> B                                          *)
 (*      to                                                                   *)