use Tactic.prove;
authorwenzelm
Sat Oct 27 23:17:46 2001 +0200 (2001-10-27)
changeset 11968859a141085d0
parent 11967 49c7f03cd311
child 11969 c850db2e2e98
use Tactic.prove;
src/HOL/Tools/typedef_package.ML
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Sat Oct 27 23:17:28 2001 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Sat Oct 27 23:17:46 2001 +0200
     1.3 @@ -90,7 +90,7 @@
     1.4        if_none witn2_tac (TRY (ALLGOALS (CLASET' blast_tac)));
     1.5    in
     1.6      message ("Proving non-emptiness of set " ^ quote (string_of_cterm cset) ^ " ...");
     1.7 -    prove_goalw_cterm [] (cterm_of (sign_of thy) goal) (K [tac])
     1.8 +    Tactic.prove (Theory.sign_of thy) [] [] goal (K tac)
     1.9    end handle ERROR => error ("Failed to prove non-emptiness of " ^ quote (string_of_cterm cset));
    1.10  
    1.11