--- a/src/HOL/arith_data.ML Fri Oct 21 18:14:37 2005 +0200
+++ b/src/HOL/arith_data.ML Fri Oct 21 18:14:38 2005 +0200
@@ -52,7 +52,7 @@
val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
fun prove_conv expand_tac norm_tac sg ss tu =
- mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
+ mk_meta_eq (OldGoals.prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
(K [expand_tac, norm_tac ss]))
handle ERROR => error ("The error(s) above occurred while trying to prove " ^
(string_of_cterm (cterm_of sg (mk_eqv tu))));