changeset 18009 | df077e122064 |
parent 18000 | ac059afd6b86 |
child 18141 | 89e2e8bed08f |
--- 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;