src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOL/List.thy	Fri Oct 21 18:14:34 2005 +0200
@@ -453,7 +453,7 @@
         val app = Const("List.op @",appT)
         val F2 = eq $ (app$lhs1$lastl) $ (app$rhs1$lastr)
         val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (F,F2));
-        val thm = Tactic.prove sg [] [] eq
+        val thm = Goal.prove sg [] [] eq
           (K (simp_tac (Simplifier.inherit_context ss rearr_ss) 1));
       in SOME ((conv RS (thm RS trans)) RS eq_reflection) end;