--- a/ProgTutorial/Solutions.thy	Mon Jun 20 13:59:58 2011 +0100
+++ b/ProgTutorial/Solutions.thy	Tue Jun 21 12:53:16 2011 +0100
@@ -35,6 +35,43 @@
 ML{*fun make_sum t1 t2 =
   HOLogic.mk_nat (HOLogic.dest_nat t1 + HOLogic.dest_nat t2) *}
 
+text {* \solution{fun:killqnt} *}
+
+ML %linenosgray{*val quantifiers = [@{const_name All}, @{const_name Ex}]
+
+fun kill_trivial_quantifiers trm =
+let
+  fun aux t =
+    case t of
+      Const (s1, T1) $ Abs (x, T2, t2) =>
+        if member (op =) quantifiers s1 andalso not (loose_bvar1 (t2, 0)) 
+        then incr_boundvars ~1 (aux t2)
+        else Const (s1, T1) $ Abs (x, T2, aux t2)
+    | t1 $ t2 => aux t1 $ aux t2
+    | Abs (s, T, t') => Abs (s, T, aux t')
+    | _ => t
+in 
+  aux trm
+end*}
+
+text {*
+  In line 7 we traverse the term, by first checking whether a term is an
+  application of a constant with an abstraction. If the constant stands for
+  a listed quantifier (see Line 1) and the bound variable does not occur
+  as a loose bound variable in the body, then we delete the quantifier. 
+  For this we have to increase all other dangling de Bruijn indices by
+  @{text "-1"} to account for the deleted quantifier. An example is 
+  as follows:
+
+  @{ML_response_fake [display,gray]
+  "@{prop \"\<forall>x y z. P x = P z\"}
+  |> kill_trivial_quantifiers
+  |> pretty_term @{context} 
+  |> pwriteln"
+  "\<forall>x z. P x = P z"}
+*}
+
+
 
 text {* \solution{fun:makelist} *}