243 val setup =

   243 val setup =

   244   Attrib.setup @{binding fundef_cong}

   244   Attrib.setup @{binding fundef_cong}

   245     (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)

   245     (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)

   246     "declaration of congruence rule for function definitions"

   246     "declaration of congruence rule for function definitions"

   247   #> setup_case_cong

   247   #> setup_case_cong

   249   #> Function_Common.Termination_Simps.setup

   248   #> Function_Common.Termination_Simps.setup

   250 

   249 

   251 val get_congs = Function_Ctx_Tree.get_function_congs

   250 val get_congs = Function_Ctx_Tree.get_function_congs

   252 

   251 

   253 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t

   252 fun get_info ctxt t = Item_Net.retrieve (get_function ctxt) t