src/HOL/Tools/Datatype/rep_datatype.ML
changeset 51673 4dfa00e264d8
parent 51672 d5c5e088ebdf
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Jan 22 13:32:41 2013 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/rep_datatype.ML	Tue Jan 22 14:33:45 2013 +0100
     1.3 @@ -518,6 +518,12 @@
     1.4      val unnamed_rules = map (fn induct =>
     1.5        ((Binding.empty, [Rule_Cases.inner_rule, Induct.induct_type ""]), [([induct], [])]))
     1.6          (drop (length dt_names) inducts);
     1.7 +
     1.8 +    val ctxt = Proof_Context.init_global thy9;
     1.9 +    val case_combs = map (Proof_Context.read_const ctxt false dummyT) case_names;
    1.10 +    val constrss = map (fn (dtname, {descr, index, ...}) =>
    1.11 +      map (Proof_Context.read_const ctxt false dummyT o fst)
    1.12 +        (#3 (the (AList.lookup op = descr index)))) dt_infos
    1.13    in
    1.14      thy9
    1.15      |> Global_Theory.note_thmss ""
    1.16 @@ -535,6 +541,7 @@
    1.17            named_rules @ unnamed_rules)
    1.18      |> snd
    1.19      |> Datatype_Data.register dt_infos
    1.20 +    |> Context.theory_map (fold2 Case_Translation.register case_combs constrss)
    1.21      |> Datatype_Data.interpretation_data (config, dt_names)
    1.22      |> pair dt_names
    1.23    end;