# HG changeset patch
# User haftmann
# Date 1423940246 -3600
# Node ID 0a528e3aad281e1e3428de0f053afa435db4d3f2
# Parent  f5de6e207d1d05463d8125ff142f288143bddfc7
only collapse patterns with disjunctive variable names

diff -r f5de6e207d1d -r 0a528e3aad28 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Feb 14 19:57:24 2015 +0100
+++ b/src/Tools/Code/code_thingol.ML	Sat Feb 14 19:57:26 2015 +0100
@@ -674,6 +674,10 @@
       else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
     fun casify constrs ty t_app ts =
       let
+        fun disjunctive_varnames ts =
+          let
+            val vs = (fold o fold_varnames) (insert (op =)) ts [];
+          in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end;
         fun collapse_clause vs_map ts body =
           case body
            of IConst { sym = Constant c, ... } => if member (op =) undefineds c
@@ -682,6 +686,7 @@
             | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
                 if forall (fn (pat', body') => exists_var pat' v
                   orelse not (exists_var body' v)) clauses
+                  andalso forall (disjunctive_varnames ts o fst) clauses
                 then case AList.lookup (op =) vs_map v
                  of SOME i => maps (fn (pat', body') =>
                       collapse_clause (AList.delete (op =) v vs_map)