diff -r 71225f4a4635 -r 282fe9cc278e Quot/quotient_term.ML --- a/Quot/quotient_term.ML Fri Jan 01 01:08:19 2010 +0100 +++ b/Quot/quotient_term.ML Fri Jan 01 01:10:38 2010 +0100 @@ -64,7 +64,6 @@ (* *) (* for example for: ?'a list *) (* it produces: %a. map a *) -(* fun mk_mapfun ctxt vs ty = let val vs' = map (mk_Free) vs