--- a/src/HOL/Tools/Presburger/presburger.ML Wed Jun 13 00:01:51 2007 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Wed Jun 13 00:01:54 2007 +0200
@@ -50,7 +50,7 @@
| _ => false)
in
if ntac then no_tac st
- else rtac (Goal.prove_raw [] g (K (blast_tac HOL_cs 1))) i st
+ else rtac (Goal.prove_internal [] g (K (blast_tac HOL_cs 1))) i st
end;
local
@@ -198,4 +198,4 @@
THEN core_cooper_tac ctxt i THEN finish_tac elim i
end;
-end;
\ No newline at end of file
+end;
--- a/src/HOL/Tools/res_axioms.ML Wed Jun 13 00:01:51 2007 +0200
+++ b/src/HOL/Tools/res_axioms.ML Wed Jun 13 00:01:54 2007 +0200
@@ -406,7 +406,7 @@
val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
and conc = c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
fun tacf [prem] = rewrite_goals_tac [def] THEN rtac (prem RS someI_ex) 1
- in Goal.prove_raw [ex_tm] conc tacf
+ in Goal.prove_internal [ex_tm] conc tacf
|> forall_intr_list frees
|> forall_elim_vars 0 (*Introduce Vars, but don't discharge defs.*)
|> Thm.varifyT