--- 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));