src/HOL/Tools/res_axioms.ML

 fun transform_elim th =
   if is_elimR th then
     let val tm = elimR2Fol th
 	val ctm = cterm_of (sign_of_thm th) tm	
     in
-	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
+	OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
     end
  else th;
 
 
 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)

       val {sign,t, ...} = rep_cterm chil
       val (Const ("Hilbert_Choice.Eps", Type("fun",[_,T]))) = t
       val cex = Thm.cterm_of sign (HOLogic.exists_const T)
       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
-  in  prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
+  in  OldGoals.prove_goalw_cterm [def] (Drule.mk_implies (ex_tm, conc))
 	    (fn [prem] => [ rtac (prem RS someI_ex) 1 ])
   end;	 
 
 
 (*Converts an Isabelle theorem (intro, elim or simp format) into nnf.*)