src/HOL/Integ/cooper_proof.ML
changeset 17959 8db36a108213
parent 17485 c39871c52977
child 17985 d5d576b72371
     1.1 --- a/src/HOL/Integ/cooper_proof.ML	Fri Oct 21 18:14:37 2005 +0200
     1.2 +++ b/src/HOL/Integ/cooper_proof.ML	Fri Oct 21 18:14:38 2005 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4      fun check NONE = error "prove_goal: tactic failed"
     1.5        | check (SOME (thm, _)) = (case nprems_of thm of
     1.6              0 => thm
     1.7 -          | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     1.8 +          | i => !OldGoals.result_error_fn thm (string_of_int i ^ " unsolved goals!"))
     1.9    in check (Seq.pull (EVERY tacs (trivial G))) end;
    1.10  
    1.11  (*-------------------------------------------------------------*)