src/HOL/Tools/function_package/fundef_package.ML
changeset 22846 fb79144af9a3
parent 22733 0b14bb35be90
child 23189 4574ab8f3b21
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -208,13 +208,11 @@
     1.4  (* setup *)
     1.5  
     1.6  val setup =
     1.7 -    FundefData.init
     1.8 -      #> FundefCongs.init
     1.9 -      #> TerminationRule.init
    1.10 -      #>  Attrib.add_attributes
    1.11 -            [("fundef_cong", Attrib.add_del_args cong_add cong_del, "declaration of congruence rule for function definitions")]
    1.12 -      #> setup_case_cong_hook
    1.13 -      #> FundefRelation.setup
    1.14 +  Attrib.add_attributes
    1.15 +    [("fundef_cong", Attrib.add_del_args cong_add cong_del,
    1.16 +      "declaration of congruence rule for function definitions")]
    1.17 +  #> setup_case_cong_hook
    1.18 +  #> FundefRelation.setup
    1.19  
    1.20  val get_congs = FundefCommon.get_fundef_congs o Context.Theory
    1.21