src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/Fun.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -497,7 +497,7 @@
       (fn sg => fn ss => fn t =>
         case find_double t of (T, NONE) => NONE
         | (T, SOME rhs) =>
-            SOME (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
+            SOME (Goal.prove sg [] [] (Term.equals T $ t $ rhs) (K (fun_upd_prover ss))))
 end;
 Addsimprocs[fun_upd2_simproc];