src/HOL/Tools/Function/function.ML
changeset 55085 0e8e4dc55866
parent 54883 dd04a8b654fc
child 55404 5cb95b79a51f
     1.1 --- a/src/HOL/Tools/Function/function.ML	Mon Jan 20 20:42:43 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Mon Jan 20 21:32:41 2014 +0100
     1.3 @@ -278,10 +278,7 @@
     1.4  (* setup *)
     1.5  
     1.6  val setup =
     1.7 -  Attrib.setup @{binding fundef_cong}
     1.8 -    (Attrib.add_del Function_Ctx_Tree.cong_add Function_Ctx_Tree.cong_del)
     1.9 -    "declaration of congruence rule for function definitions"
    1.10 -  #> setup_case_cong
    1.11 +  setup_case_cong
    1.12    #> Function_Common.Termination_Simps.setup
    1.13  
    1.14  val get_congs = Function_Ctx_Tree.get_function_congs