src/HOL/Tools/ctr_sugar.ML
changeset 54635 30666a281ae3
parent 54634 366297517091
child 54691 506312c293f5
equal deleted inserted replaced
54634:366297517091 54635:30666a281ae3
   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