# HG changeset patch
# User wenzelm
# Date 1004217466 -7200
# Node ID 859a141085d0dc404213544f3e9cd248c238c295
# Parent  49c7f03cd311d0d244aca372baec7993304ce4d3
use Tactic.prove;

diff -r 49c7f03cd311 -r 859a141085d0 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sat Oct 27 23:17:28 2001 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 27 23:17:46 2001 +0200
@@ -90,7 +90,7 @@
       if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
   in
     message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
-    prove_goalw_cterm [] (cterm_of (sign_of thy) goal) (K [tac])
+    Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
   end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));