added failure cases for poly

012_systemf.md

@@ -250,8 +250,6 @@ Substitution
 Erasure
 -------
 
-The type erasure:
-
 $$
 \begin{aligned}[lcl]
 & \t{erase}(x)      &=&\ x \\
@@ -269,6 +267,6 @@ unbound-generics
 ----------------
 
 Up until now we've been writing our own binding implementation. There is however
-a better way
+a better way to automate writing a lot of the substitution boilerplate.
 
 \clearpage

chapter7/poly/fail2.ml

@@ -0,0 +1,4 @@
+let f = (\x -> if x then x else (x+1));
+let g = (\x -> if x then 1 else (x+1));
+let h = (\x -> if x then (x+1) else 1);
+let j = (\x -> fix (x 0));