clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;

--- a/src/HOL/Inductive.thy	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Inductive.thy	Thu Dec 15 18:08:40 2011 +0100
@@ -11,9 +11,9 @@
   "Tools/dseq.ML"
   "Tools/Datatype/datatype_aux.ML"
   "Tools/Datatype/datatype_prop.ML"
-  "Tools/Datatype/datatype_case.ML"
   ("Tools/Datatype/datatype_abs_proofs.ML")
   ("Tools/Datatype/datatype_data.ML")
+  ("Tools/Datatype/datatype_case.ML")
   ("Tools/Datatype/rep_datatype.ML")
   ("Tools/primrec.ML")
   ("Tools/Datatype/datatype_codegen.ML")
@@ -277,9 +277,8 @@
 text {* Package setup. *}
 
 use "Tools/Datatype/datatype_abs_proofs.ML"
-use "Tools/Datatype/datatype_data.ML"
-setup Datatype_Data.setup
-
+use "Tools/Datatype/datatype_data.ML" setup Datatype_Data.setup
+use "Tools/Datatype/datatype_case.ML" setup Datatype_Case.setup
 use "Tools/Datatype/rep_datatype.ML"
 
 use "Tools/Datatype/datatype_codegen.ML"
@@ -300,7 +299,7 @@
     let
       (* FIXME proper name context!? *)
       val x = Free (singleton (Name.variant_list (Term.add_free_names cs [])) "x", dummyT);
-      val ft = Datatype_Case.case_tr true Datatype_Data.info_of_constr_permissive ctxt [x, cs];
+      val ft = Datatype_Case.case_tr true ctxt [x, cs];
     in lambda x ft end
 in [(@{syntax_const "_lam_pats_syntax"}, fun_tr)] end
 *}

--- a/src/HOL/List.thy	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/List.thy	Thu Dec 15 18:08:40 2011 +0100
@@ -391,7 +391,7 @@
         Syntax.const @{syntax_const "_case1"} $
           Syntax.const @{const_syntax dummy_pattern} $ NilC;
       val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
-      val ft = Datatype_Case.case_tr false Datatype.info_of_constr_permissive ctxt [x, cs];
+      val ft = Datatype_Case.case_tr false ctxt [x, cs];
     in lambda x ft end;
 
   fun abs_tr ctxt (p as Free (s, T)) e opti =

--- a/src/HOL/Tools/Datatype/datatype_case.ML	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_case.ML	Thu Dec 15 18:08:40 2011 +0100
@@ -9,17 +9,12 @@
 sig
   datatype config = Error | Warning | Quiet
   type info = Datatype_Aux.info
-  val make_case: (string * typ -> info option) ->
-    Proof.context -> config -> string list -> term -> (term * term) list ->
-    term
-  val dest_case: (string -> info option) -> bool ->
-    string list -> term -> (term * (term * term) list) option
-  val strip_case: (string -> info option) -> bool ->
-    term -> (term * (term * term) list) option
-  val case_tr: bool -> (theory -> string * typ -> info option) ->
-    Proof.context -> term list -> term
-  val case_tr': (theory -> string -> info option) ->
-    string -> Proof.context -> term list -> term
+  val make_case :  Proof.context -> config -> string list -> term -> (term * term) list -> term
+  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
+  val case_tr: bool -> Proof.context -> term list -> term
+  val case_tr': string -> Proof.context -> term list -> term
+  val add_case_tr' : string list -> theory -> theory
+  val setup: theory -> theory
 end;
 
 structure Datatype_Case : DATATYPE_CASE =
@@ -147,8 +142,10 @@
 
 (* Translation of pattern terms into nested case expressions. *)
 
-fun mk_case tab ctxt ty_match ty_inst type_of used range_ty =
+fun mk_case ctxt ty_match ty_inst type_of used range_ty =
   let
+    val tab = Datatype_Data.info_of_constr_permissive (Proof_Context.theory_of ctxt);
+
     val name = singleton (Name.variant_list used) "a";
     fun expand constructors used ty ((_, []), _) = raise CASE_ERROR ("mk_case: expand_var_row", ~1)
       | expand constructors used ty (row as ((prfx, p :: ps), (rhs, tag))) =
@@ -215,7 +212,7 @@
         else x :: xs)
     | _ => I) pat [];
 
-fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses =
+fun gen_make_case ty_match ty_inst type_of ctxt config used x clauses =
   let
     fun string_of_clause (pat, rhs) =
       Syntax.string_of_term ctxt (Syntax.const @{syntax_const "_case1"} $ pat $ rhs);
@@ -228,7 +225,7 @@
       | _ => case_error "all cases must have the same result type");
     val used' = fold add_row_used rows used;
     val (tags, case_tm) =
-      mk_case tab ctxt ty_match ty_inst type_of used' rangeT [x] rows
+      mk_case ctxt ty_match ty_inst type_of used' rangeT [x] rows
         handle CASE_ERROR (msg, i) =>
           case_error
             (msg ^ (if i < 0 then "" else "\nIn clause\n" ^ string_of_clause (nth clauses i)));
@@ -245,9 +242,9 @@
 
 in
 
-fun make_case tab ctxt =
+fun make_case ctxt =
   gen_make_case (match_type (Proof_Context.theory_of ctxt))
-    Envir.subst_term_types fastype_of tab ctxt;
+    Envir.subst_term_types fastype_of ctxt;
 
 val make_case_untyped =
   gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT);
@@ -257,7 +254,7 @@
 
 (* parse translation *)
 
-fun case_tr err tab_of ctxt [t, u] =
+fun case_tr err ctxt [t, u] =
       let
         val thy = Proof_Context.theory_of ctxt;
         val intern_const_syntax = Consts.intern_syntax (Proof_Context.consts_of ctxt);
@@ -291,12 +288,17 @@
           | 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
+          make_case_untyped ctxt
             (if err then Error else Warning) []
             (fold (fn tT => fn t => Syntax.const @{syntax_const "_constrain"} $ t $ tT)
                (flat cnstrts) t) cases;
       in case_tm end
-  | case_tr _ _ _ ts = case_error "case_tr";
+  | case_tr _ _ ts = case_error "case_tr";
+
+val trfun_setup =
+  Sign.add_advanced_trfuns ([],
+    [(@{syntax_const "_case_syntax"}, case_tr true)],
+    [], []);
 
 
 (* Pretty printing of nested case expressions *)
@@ -306,7 +308,7 @@
 local
 
 (* FIXME proper name context!? *)
-fun gen_dest_case name_of type_of tab d used t =
+fun gen_dest_case name_of type_of ctxt d used t =
   (case apfst name_of (strip_comb t) of
     (SOME cname, ts as _ :: _) =>
       let
@@ -328,6 +330,7 @@
           | count_cases (c, (_, body), false) = AList.map_default op aconv (body, []) (cons c);
         val is_undefined = name_of #> equal (SOME @{const_name undefined});
         fun mk_case (c, (xs, body), _) = (list_comb (c, xs), body);
+        val tab = Datatype_Data.info_of_case (Proof_Context.theory_of ctxt);
       in
         (case ty_info tab cname of
           SOME {constructors, case_name} =>
@@ -409,9 +412,10 @@
 
 (* print translation *)
 
-fun case_tr' tab_of cname ctxt ts =
+fun case_tr' cname ctxt ts =
   let
     val thy = Proof_Context.theory_of ctxt;
+
     fun mk_clause (pat, rhs) =
       let val xs = Term.add_frees pat [] in
         Syntax.const @{syntax_const "_case1"} $
@@ -424,7 +428,7 @@
               | t => t) rhs
       end;
   in
-    (case strip_case' (tab_of thy) true (list_comb (Syntax.const cname, ts)) of
+    (case strip_case' ctxt true (list_comb (Syntax.const cname, ts)) of
       SOME (x, clauses) =>
         Syntax.const @{syntax_const "_case_syntax"} $ x $
           foldr1 (fn (t, u) => Syntax.const @{syntax_const "_case2"} $ t $ u)
@@ -432,4 +436,15 @@
     | NONE => raise Match)
   end;
 
+fun add_case_tr' case_names thy =
+  Sign.add_advanced_trfuns ([], [],
+    map (fn case_name =>
+      let val case_name' = Lexicon.mark_const case_name
+      in (case_name', case_tr' case_name') end) case_names, []) thy;
+
+
+(* theory setup *)
+
+val setup = trfun_setup;
+
 end;

--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Dec 15 18:08:40 2011 +0100
@@ -24,10 +24,6 @@
   val mk_case_names_exhausts: descr -> string list -> attribute list
   val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
   val interpretation_data : config * string list -> theory -> theory
-  val make_case :  Proof.context -> Datatype_Case.config -> string list -> term ->
-    (term * term) list -> term
-  val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
-  val add_case_tr' : string list -> theory -> theory
   val setup: theory -> theory
 end;
 
@@ -198,27 +194,6 @@
 end;
 
 
-(* translation rules for case *)
-
-fun make_case ctxt =
-  Datatype_Case.make_case (info_of_constr_permissive (Proof_Context.theory_of ctxt)) ctxt;
-
-fun strip_case ctxt =
-  Datatype_Case.strip_case (info_of_case (Proof_Context.theory_of ctxt));
-
-fun add_case_tr' case_names thy =
-  Sign.add_advanced_trfuns ([], [],
-    map (fn case_name =>
-      let val case_name' = Lexicon.mark_const case_name in
-        (case_name', Datatype_Case.case_tr' info_of_case case_name')
-      end) case_names, []) thy;
-
-val trfun_setup =
-  Sign.add_advanced_trfuns ([],
-    [(@{syntax_const "_case_syntax"}, Datatype_Case.case_tr true info_of_constr_permissive)],
-    [], []);
-
-
 
 (** document antiquotation **)
 
@@ -262,7 +237,6 @@
 (** setup theory **)
 
 val setup =
-  trfun_setup #>
   antiq_setup #>
   Datatype_Interpretation.init;
 

--- a/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Thu Dec 15 18:08:40 2011 +0100
@@ -99,9 +99,9 @@
         ((Binding.empty, flat (distinct @ inject)), [Induct.induct_simp_add])] @
           named_rules @ unnamed_rules)
     |> snd
-    |> Datatype_Data.add_case_tr' case_names
     |> Datatype_Data.register dt_infos
     |> Datatype_Data.interpretation_data (config, dt_names)
+    |> Datatype_Case.add_case_tr' case_names
     |> pair dt_names
   end;
 

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Dec 15 18:08:40 2011 +0100
@@ -663,7 +663,7 @@
     val v = Free (name, T);
     val v' = Free (name', T);
   in
-    lambda v (Datatype.make_case ctxt Datatype_Case.Quiet [] v
+    lambda v (Datatype_Case.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) $
@@ -949,7 +949,7 @@
         in
           (pattern, compilation)
         end
-        val switch = Datatype.make_case ctxt Datatype_Case.Quiet [] inp_var
+        val switch = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] inp_var
           ((map compile_single_case switched_clauses) @
             [(xt, mk_empty compfuns (HOLogic.mk_tupleT outTs))])
       in

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 15 17:37:14 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 15 18:08:40 2011 +0100
@@ -412,7 +412,7 @@
   end
 
 fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) =
-    Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
+    Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) =>
       (t, mk_case_term ctxt (p - 1) qs' c)) cs)
   | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) =
     if p = 0 then t else mk_case_term ctxt (p - 1) qs' c