# HG changeset patch
# User paulson
# Date 1130494954 -7200
# Node ID df077e122064a9bcc847b6d9c801df3ff2c51c7a
# Parent  f193815cab2c35bc746d6fb69c757ce0182f45ec
got rid of obsolete prove_goalw_cterm

diff -r f193815cab2c -r df077e122064 src/HOL/Tools/res_axioms.ML
--- 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;