got rid of obsolete prove_goalw_cterm

--- a/src/HOL/Tools/res_axioms.ML	Fri Oct 28 09:36:19 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri Oct 28 12:22:34 2005 +0200
@@ -136,9 +136,7 @@
   if is_elimR th then
     let val tm = elimR2Fol th
 	val ctm = cterm_of (sign_of_thm th) tm	
-    in
-	OldGoals.prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
-    end
+    in Goal.prove_raw [] ctm (fn _ => elimRule_tac th) end
  else th;