# HG changeset patch
# User krauss
# Date 1307484080 -7200
# Node ID fa3c61dc9f2cb760ab61c39953a41893e716e951
# Parent  b142ae3e9478a0f2bca7dc242040ecf1a63ffba2
removed generation of instantiated pattern set, which is never actually used

diff -r b142ae3e9478 -r fa3c61dc9f2c src/HOL/Tools/Datatype/datatype_case.ML
--- a/src/HOL/Tools/Datatype/datatype_case.ML	Wed Jun 08 00:01:20 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Wed Jun 08 00:01:20 2011 +0200
@@ -11,7 +11,7 @@
   type info = Datatype_Aux.info
   val make_case: (string * typ -> info option) ->
     Proof.context -> config -> string list -> term -> (term * term) list ->
-    term * (term * (int * bool)) list
+    term
   val dest_case: (string -> info option) -> bool ->
     string list -> term -> (term * (term * term) list) option
   val strip_case: (string -> info option) -> bool ->
@@ -164,20 +164,9 @@
  * Misc. routines used in mk_case
  *---------------------------------------------------------------------------*)
 
-fun mk_pat ((c, c'), l) =
-  let
-    val L = length (binder_types (fastype_of c))
-    fun build (prfx, tag, plist) =
-      let val (args, plist') = chop L plist
-      in (prfx, tag, list_comb (c', args) :: plist') end
-  in map build l end;
-
 fun v_to_prfx (prfx, Free v::pats) = (v::prfx,pats)
   | v_to_prfx _ = raise CASE_ERROR ("mk_case: v_to_prfx", ~1);
 
-fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, Free v::pats)
-  | v_to_pats _ = raise CASE_ERROR ("mk_case: v_to_pats", ~1);
-
 
 (*----------------------------------------------------------------------------
  * Translation of pattern terms into nested case expressions.
@@ -205,7 +194,7 @@
           else [row]
     fun mk {rows = [], ...} = raise CASE_ERROR ("no rows", ~1)
       | mk {path = [], rows = ((prfx, []), (tm, tag)) :: _} =  (* Done *)
-          ([(prfx, tag, [])], tm)
+          ([tag], tm)
       | mk {path, rows as ((row as ((_, [Free _]), _)) :: _ :: _)} =
           mk {path = path, rows = [row]}
       | mk {path = u :: rstp, rows as ((_, _ :: _), _) :: _} =
@@ -215,8 +204,7 @@
                 let
                   val rows' = map (fn ((v, _), row) => row ||>
                     pattern_subst [(v, u)] |>> v_to_prfx) (col0 ~~ rows);
-                  val (pref_patl, tm) = mk {path = rstp, rows = rows'}
-                in (map v_to_pats pref_patl, tm) end
+                in mk {path = rstp, rows = rows'} end
             | SOME (Const (cname, cT), i) =>
                 (case ty_info tab (cname, cT) of
                   NONE => raise CASE_ERROR ("Not a datatype constructor: " ^ cname, i)
@@ -227,7 +215,6 @@
                     val nrows = maps (expand constructors used' pty) rows;
                     val subproblems = partition ty_match ty_inst type_of used'
                       constructors pty range_ty nrows;
-                    val constructors' = map #constructor subproblems
                     val news = map (fn {new_formals, group, ...} =>
                       {path = new_formals @ rstp, rows = group}) subproblems;
                     val (pat_rect, dtrees) = split_list (map mk news);
@@ -242,8 +229,7 @@
                     val types = map type_of (case_functions @ [u]);
                     val case_const = Const (case_name, types ---> range_ty)
                     val tree = list_comb (case_const, case_functions @ [u])
-                    val pat_rect1 = maps mk_pat (constructors ~~ constructors' ~~ pat_rect)
-                  in (pat_rect1, tree) end)
+                  in (flat pat_rect, tree) end)
             | SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
                 Syntax.string_of_term ctxt t, i))
           end
@@ -274,16 +260,12 @@
       | [T] => T
       | _ => case_error "all cases must have the same result type");
     val used' = fold add_row_used rows used;
-    val (patts, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
+    val (tags, case_tm) = mk_case tab ctxt ty_match ty_inst type_of
         used' rangeT {path = [x], rows = rows}
       handle CASE_ERROR (msg, i) => case_error (msg ^
         (if i < 0 then ""
          else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
-    val patts1 = map
-      (fn (_, tag, [pat]) => (pat, tag)
-        | _ => case_error "error in pattern-match translation") patts;
-    val patts2 = Library.sort (int_ord o pairself row_of_pat) patts1
-    val finals = map row_of_pat patts2
+    val finals = map fst tags
     val originals = map (row_of_pat o #2) rows
     val _ =
       (case subtract (op =) finals originals of
@@ -293,7 +275,7 @@
             ("The following clauses are redundant (covered by preceding clauses):\n" ^
              cat_lines (map (string_of_clause o nth clauses) is)));
   in
-    (case_tm, patts2)
+    case_tm
   end;
 
 fun make_case tab ctxt = gen_make_case
@@ -340,7 +322,7 @@
         fun dest_case2 (Const (@{syntax_const "_case2"}, _) $ t $ u) = t :: dest_case2 u
           | dest_case2 t = [t];
         val (cases, cnstrts) = split_list (map dest_case1 (dest_case2 u));
-        val (case_tm, _) = make_case_untyped (tab_of thy) ctxt
+        val case_tm = make_case_untyped (tab_of thy) ctxt
           (if err then Error else Warning) []
           (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
              (flat cnstrts) t) cases;
diff -r b142ae3e9478 -r fa3c61dc9f2c src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Jun 08 00:01:20 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Jun 08 00:01:20 2011 +0200
@@ -26,7 +26,7 @@
   val info_of_case : theory -> string -> info option
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val make_case :  Proof.context -> Datatype_Case.config -> string list -> term ->
-    (term * term) list -> term * (term * (int * bool)) list
+    (term * term) list -> term
   val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
   val read_typ: theory -> string -> (string * sort) list -> typ * (string * sort) list
   val cert_typ: theory -> typ -> (string * sort) list -> typ * (string * sort) list
diff -r b142ae3e9478 -r fa3c61dc9f2c src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 08 00:01:20 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Jun 08 00:01:20 2011 +0200
@@ -634,13 +634,13 @@
     val v = Free (name, T);
     val v' = Free (name', T);
   in
-    lambda v (fst (Datatype.make_case ctxt Datatype_Case.Quiet [] v
+    lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v
       [(HOLogic.mk_tuple out_ts,
         if null eqs'' then success_t
         else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
           foldr1 HOLogic.mk_conj eqs'' $ success_t $
             mk_bot compfuns U'),
-       (v', mk_bot compfuns U')]))
+       (v', mk_bot compfuns U')])
   end;
 
 fun string_of_tderiv ctxt (t, deriv) = 
@@ -920,9 +920,9 @@
         in
           (pattern, compilation)
         end
-        val switch = fst (Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
+        val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
           ((map compile_single_case switched_clauses) @
-            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))]))
+            [(xt, mk_bot compfuns (HOLogic.mk_tupleT outTs))])
       in
         case compile_switch_tree all_vs ctxt_eqs left_clauses of
           NONE => SOME switch