Loader = Deb_sn + consts appl :: "deriv => deriv list => deriv" rappl :: "deriv => deriv list => deriv" primrec appl_Cons "appl f (a # as) = appl (Mp f a) as" appl_Nil "appl f [] = f" primrec rappl_Cons "rappl f (a # as) = Mp (rappl f as) a" rappl_Nil "rappl f [] = f" end