# HG changeset patch
# User wenzelm
# Date 1214257544 -7200
# Node ID 5c66afff695ef8eb5f0c24bfa33fb5ed3dd838ea
# Parent  1af2598b5f7d419e045f3afca1c4647c44d3baed
Term.all;

diff -r 1af2598b5f7d -r 5c66afff695e src/HOLCF/Tools/adm_tac.ML
--- 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));