src/HOLCF/adm_tac.ML

        val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
        fun mk_all [] t = t
          | 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 = Goal.prove sign [] [] t' (K (tac 1));
+       val thm = Goal.prove (ProofContext.init sign) [] [] t' (K (tac 1));
   in (ts, thm)::l end
   handle ERROR _ => l;
 
 
 (*** instantiation of adm_subst theorem (a bit tricky) ***)