# HG changeset patch
# User blanchet
# Date 1392190556 -3600
# Node ID f3353672399936e246d1b23c04a1d4d8f4c63177
# Parent  1e8dd9cd320bf87ad0589efb6fb6970d01ac7a92
more 'ctr_sugar' modernization

diff -r 1e8dd9cd320b -r f33536723999 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Feb 12 08:35:56 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Feb 12 08:35:56 2014 +0100
@@ -13,15 +13,11 @@
 
 fun add_code_for_datatype fcT_name thy =
   let
-    val (As', ctr_specs) = Datatype_Data.the_spec thy fcT_name;
-    val {inject = inject_thms, distinct = distinct_thms, case_rewrites = case_thms, ...} =
-      Datatype_Data.the_info thy fcT_name;
-
-    val As = map TFree As';
-    val fcT = Type (fcT_name, As);
-    val ctrs = map (fn (c, arg_Ts) => (c, arg_Ts ---> fcT)) ctr_specs;
+    val ctxt = Proof_Context.init_global thy
+    val SOME {ctrs, injects, distincts, case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt fcT_name
+    val Type (_, As) = body_type (fastype_of (hd ctrs))
   in
-    Ctr_Sugar_Code.add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy
+    Ctr_Sugar_Code.add_ctr_code fcT_name As (map dest_Const ctrs) injects distincts case_thms thy
   end;
 
 val _ = Theory.setup (Datatype_Data.interpretation (K (fold add_code_for_datatype)));