src/HOLCF/adm_tac.ML

--- a/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:32 2005 +0200
+++ b/src/HOLCF/adm_tac.ML	Fri Oct 21 18:14:34 2005 +0200
@@ -102,7 +102,7 @@
          | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
        val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
        val t' = mk_all params (Logic.list_implies (prems, t));
-       val thm = Tactic.prove sign [] [] t' (K (tac 1));
+       val thm = Goal.prove sign [] [] t' (K (tac 1));
   in (ts, thm)::l end
   handle ERROR_MESSAGE _ => l;