# HG changeset patch
# User haftmann
# Date 1423984664 -3600
# Node ID d3f4ddeaacc344ca1a78d773cc7cc80660da4b0a
# Parent  0a528e3aad281e1e3428de0f053afa435db4d3f2
purge variables not mentioned in body from pattern

diff -r 0a528e3aad28 -r d3f4ddeaacc3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Feb 14 19:57:26 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sun Feb 15 08:17:44 2015 +0100
@@ -678,6 +678,13 @@
           let
             val vs = (fold o fold_varnames) (insert (op =)) ts [];
           in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end;
+        fun purge_unused_vars_in t =
+          let
+            val vs = fold_varnames (insert (op =)) t [];
+          in
+            map_terms_bottom_up (fn IVar (SOME v) =>
+              IVar (if member (op =) vs v then SOME v else NONE) | t => t)
+          end;
         fun collapse_clause vs_map ts body =
           case body
            of IConst { sym = Constant c, ... } => if member (op =) undefineds c
@@ -690,7 +697,7 @@
                 then case AList.lookup (op =) vs_map v
                  of SOME i => maps (fn (pat', body') =>
                       collapse_clause (AList.delete (op =) v vs_map)
-                        (nth_map i (K pat') ts) body') clauses
+                        (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses
                   | NONE => [(ts, body)]
                 else [(ts, body)]
             | _ => [(ts, body)];