--- a/src/HOLCF/Tools/adm_tac.ML Mon Jun 23 23:45:39 2008 +0200
+++ b/src/HOLCF/Tools/adm_tac.ML Mon Jun 23 23:45:44 2008 +0200
@@ -99,7 +99,7 @@
let val parTs = map snd (rev params);
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));
+ | mk_all ((a,T)::Ts) t = Term.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 (ProofContext.init sign) [] [] t' (K (tac 1));