# HG changeset patch
# User wenzelm
# Date 1181685714 -7200
# Node ID 356edb5eb1c4a85f448745a5938c97d7167ac9bc
# Parent  3702086a15a391de2bf6e3558051939037ec8ecf
renamed Goal.prove_raw to Goal.prove_internal;

diff -r 3702086a15a3 -r 356edb5eb1c4 src/HOL/Tools/Presburger/presburger.ML
--- 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;
diff -r 3702086a15a3 -r 356edb5eb1c4 src/HOL/Tools/res_axioms.ML
--- 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