keep a database of free constructor type information

--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 10:26:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Wed Sep 25 10:45:12 2013 +0200
@@ -30,6 +30,7 @@
      case_conv_ifs: thm list};
 
   val morph_ctr_sugar: morphism -> ctr_sugar -> ctr_sugar
+  val ctr_sugar_of: Proof.context -> string -> ctr_sugar option
 
   val rep_compat_prefix: string
 
@@ -103,6 +104,27 @@
    expands = map (Morphism.thm phi) expands,
    case_conv_ifs = map (Morphism.thm phi) case_conv_ifs};
 
+fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
+    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
+  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
+
+structure Data = Generic_Data
+(
+  type T = ctr_sugar Symtab.table;
+  val empty = Symtab.empty;
+  val extend = I;
+  val merge = Symtab.merge eq_ctr_sugar;
+);
+
+fun ctr_sugar_of ctxt =
+  Symtab.lookup (Data.get (Context.Proof ctxt))
+  #> Option.map (morph_ctr_sugar
+    (Morphism.thm_morphism (Thm.transfer (Proof_Context.theory_of ctxt))));
+
+fun register_ctr_sugar key ctr_sugar =
+  Local_Theory.declaration {syntax = false, pervasive = true}
+    (fn phi => Data.map (Symtab.default (key, morph_ctr_sugar phi ctr_sugar)));
+
 val rep_compat_prefix = "new";
 
 val isN = "is_";
@@ -787,19 +809,23 @@
         val notes' =
           [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+        val ctr_sugar =
+          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+           nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
+           case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
+           split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
+           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
+           collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms};
       in
-        ({ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
-          nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
-          case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
-          split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
-          discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
-          collapses = all_collapse_thms, expands = expand_thms, case_conv_ifs = case_conv_if_thms},
+        (ctr_sugar,
          lthy
          |> not rep_compat ?
             (Local_Theory.declaration {syntax = false, pervasive = true}
                (fn phi => Case_Translation.register
                   (Morphism.term phi casex) (map (Morphism.term phi) ctrs)))
-         |> Local_Theory.notes (notes' @ notes) |> snd)
+         |> Local_Theory.notes (notes' @ notes) |> snd
+         |> register_ctr_sugar dataT_name ctr_sugar)
       end;
   in
     (goalss, after_qed, lthy')

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:26:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 10:45:12 2013 +0200
@@ -197,10 +197,7 @@
     massage_call
   end;
 
-(* TODO: also support old-style datatypes.
-   (Ideally, we would have a proper registry for these things.) *)
-fun case_of ctxt =
-  fp_sugar_of ctxt #> Option.map (fst o dest_Const o #casex o of_fp_sugar #ctr_sugars);
+fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
 
 fun fold_rev_let_if_case ctxt f bound_Ts =
   let
@@ -312,16 +309,8 @@
   end;
 
 fun expand_ctr_term ctxt s Ts t =
-  (case fp_sugar_of ctxt s of
-    SOME fp_sugar =>
-    let
-      val T = Type (s, Ts);
-      val {ctrs = ctrs0, casex = case0, ...} = of_fp_sugar #ctr_sugars fp_sugar;
-      val ctrs = map (mk_ctr Ts) ctrs0;
-      val casex = mk_case Ts T case0;
-    in
-      list_comb (casex, ctrs) $ t
-    end
+  (case ctr_sugar_of ctxt s of
+    SOME {ctrs, casex, ...} => list_comb (mk_case Ts (Type (s, Ts)) casex, map (mk_ctr Ts) ctrs) $ t
   | NONE => raise Fail "expand_ctr_term");
 
 fun expand_corec_code_rhs ctxt has_call bound_Ts t =