Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Term.all;
authorwenzelm
Mon, 23 Jun 2008 23:45:44 +0200
changeset 27331 5c66afff695e
parent 27330 1af2598b5f7d
child 27332 94790a9620c3
Term.all;
src/HOLCF/Tools/adm_tac.ML file | annotate | diff | comparison | revisions 
--- 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));
isabelle