equal
deleted
inserted
replaced
928 lthy |
928 lthy |
929 |> not rep_compat ? |
929 |> not rep_compat ? |
930 Local_Theory.declaration {syntax = false, pervasive = true} |
930 Local_Theory.declaration {syntax = false, pervasive = true} |
931 (fn phi => Case_Translation.register |
931 (fn phi => Case_Translation.register |
932 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)) |
932 (Morphism.term phi casex) (map (Morphism.term phi) ctrs)) |
933 |> Local_Theory.notes (anonymous_notes @ notes) |> snd |
|
934 |> register_ctr_sugar fcT_name ctr_sugar |
|
935 |> (not no_code andalso null (Thm.hyps_of (hd case_thms))) |
933 |> (not no_code andalso null (Thm.hyps_of (hd case_thms))) |
936 ? Local_Theory.background_theory |
934 ? Local_Theory.background_theory |
937 (add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms case_thms)) |
935 (fold (fold Code.del_eqn) [disc_defs, sel_defs] |
|
936 #> add_ctr_code fcT_name As (map dest_Const ctrs) inject_thms distinct_thms |
|
937 case_thms) |
|
938 |> Local_Theory.notes (anonymous_notes @ notes) |> snd |
|
939 |> register_ctr_sugar fcT_name ctr_sugar) |
938 end; |
940 end; |
939 in |
941 in |
940 (goalss, after_qed, lthy') |
942 (goalss, after_qed, lthy') |
941 end; |
943 end; |
942 |
944 |