More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const
Changed the TFL functor to a structure (currently called Prim)
\begin{thebibliography}{10}\bibitem{galton90}Antony Galton.\newblock {\em Logic for Information Technology}.\newblock Wiley, 1990.\bibitem{mgordon-hol}M.~J.~C. Gordon and T.~F. Melham.\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher Order Logic}.\newblock Cambridge University Press, 1993.\bibitem{mgordon79}Michael J.~C. Gordon, Robin Milner, and Christopher~P. Wadsworth.\newblock {\em Edinburgh {LCF}: A Mechanised Logic of Computation}.\newblock LNCS 78. Springer, 1979.\bibitem{haskell-tutorial}Paul Hudak and Joseph~H. Fasel.\newblock A gentle introduction to {Haskell}.\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.\bibitem{haskell-report}Paul Hudak, Simon~Peyton Jones, and Philip Wadler.\newblock Report on the programming language {Haskell}: A non-strict, purely functional language.\newblock {\em {SIGPLAN} Notices}, 27(5), May 1992.\newblock Version 1.2.\bibitem{huet75}G.~P. Huet.\newblock A unification algorithm for typed $\lambda$-calculus.\newblock {\em Theoretical Computer Science}, 1:27--57, 1975.\bibitem{miller-mixed}Dale Miller.\newblock Unification under a mixed prefix.\newblock {\em Journal of Symbolic Computation}, 14(4):321--358, 1992.\bibitem{nipkow-prehofer}Tobias Nipkow and Christian Prehofer.\newblock Type reconstruction for type classes.\newblock {\em Journal of Functional Programming}, 5(2):201--224, 1995.\bibitem{nordstrom90}Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.\newblock Oxford University Press, 1990.\bibitem{paulson-natural}Lawrence~C. Paulson.\newblock Natural deduction as higher-order resolution.\newblock {\em Journal of Logic Programming}, 3:237--258, 1986.\bibitem{paulson87}Lawrence~C. Paulson.\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.\newblock Cambridge University Press, 1987.\bibitem{paulson-found}Lawrence~C. Paulson.\newblock The foundation of a generic theorem prover.\newblock {\em Journal of Automated Reasoning}, 5(3):363--397, 1989.\bibitem{paulson700}Lawrence~C. Paulson.\newblock {Isabelle}: The next 700 theorem provers.\newblock In P.~Odifreddi, editor, {\em Logic and Computer Science}, pages 361--386. Academic Press, 1990.\bibitem{paulson91}Lawrence~C. Paulson.\newblock {\em {ML} for the Working Programmer}.\newblock Cambridge University Press, 1991.\bibitem{paulson-handbook}Lawrence~C. Paulson.\newblock Designing a theorem prover.\newblock In S.~Abramsky, D.~M. Gabbay, and T.~S.~E. Maibaum, editors, {\em Handbook of Logic in Computer Science}, volume~2, pages 415--475. Oxford University Press, 1992.\bibitem{pelletier86}F.~J. Pelletier.\newblock Seventy-five problems for testing automatic theorem provers.\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.\bibitem{reeves90}Steve Reeves and Michael Clarke.\newblock {\em Logic for Computer Science}.\newblock Addison-Wesley, 1990.\bibitem{suppes72}Patrick Suppes.\newblock {\em Axiomatic Set Theory}.\newblock Dover, 1972.\bibitem{wos-bledsoe}Larry Wos.\newblock Automated reasoning and {Bledsoe's} dream for the field.\newblock In Robert~S. Boyer, editor, {\em Automated Reasoning: Essays in Honor of {Woody Bledsoe}}, pages 297--342. Kluwer Academic Publishers, 1991.\end{thebibliography}