Handle dummy patterns in parse translation rather than check phase

--- a/src/HOL/Tools/case_translation.ML	Sat Apr 06 01:42:07 2013 +0200
+++ b/src/HOL/Tools/case_translation.ML	Tue Apr 09 18:27:49 2013 +0200
@@ -116,9 +116,22 @@
           | abs_pat (t $ u) _ = abs_pat u [] #> abs_pat t []
           | abs_pat _ _ = I;
 
-        fun dest_case1 (Const (@{syntax_const "_case1"}, _) $ l $ r) =
-              abs_pat l []
-                (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l $ r)
+        (* replace occurrences of dummy_pattern by distinct variables *)
+        fun replace_dummies (Const (@{const_syntax dummy_pattern}, T)) used =
+              let val (x, used') = Name.variant "x" used
+              in (Free (x, T), used') end
+          | replace_dummies (t $ u) used =
+              let
+                val (t', used') = replace_dummies t used;
+                val (u', used'') = replace_dummies u used';
+              in (t' $ u', used'') end
+          | replace_dummies t used = (t, used);
+
+        fun dest_case1 (t as Const (@{syntax_const "_case1"}, _) $ l $ r) =
+              let val (l', _) = replace_dummies l (Term.declare_term_frees t Name.context)
+              in abs_pat l' []
+                (Syntax.const @{const_syntax case_elem} $ Term_Position.strip_positions l' $ r)
+              end
           | dest_case1 _ = case_error "dest_case1";
 
         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
@@ -338,17 +351,6 @@
   in mk end;
 
 
-(* replace occurrences of dummy_pattern by distinct variables *)
-fun replace_dummies (Const (@{const_name dummy_pattern}, T)) used =
-      let val (x, used') = Name.variant "x" used
-      in (Free (x, T), used') end
-  | replace_dummies (t $ u) used =
-      let
-        val (t', used') = replace_dummies t used;
-        val (u', used'') = replace_dummies u used';
-      in (t' $ u', used'') end
-  | replace_dummies t used = (t, used);
-
 (*Repeated variable occurrences in a pattern are not allowed.*)
 fun no_repeat_vars ctxt pat = fold_aterms
   (fn x as Free (s, _) =>
@@ -364,13 +366,7 @@
     fun string_of_clause (pat, rhs) =
       Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
     val _ = map (no_repeat_vars ctxt o fst) clauses;
-    val (rows, used') = used |>
-      fold (fn (pat, rhs) =>
-        Term.declare_term_frees pat #> Term.declare_term_frees rhs) clauses |>
-      fold_map (fn (i, (pat, rhs)) => fn used =>
-        let val (pat', used') = replace_dummies pat used
-        in ((([], [pat']), (rhs, i)), used') end)
-          (map_index I clauses);
+    val rows = map_index (fn (i, (pat, rhs)) => (([], [pat]), (rhs, i))) clauses;
     val rangeT =
       (case distinct (op =) (map (fastype_of o snd) clauses) of
         [] => case_error "no clauses given"