src/HOL/Tools/Function/fundef.ML
changeset 31902 862ae16a799d
parent 31784 bd3486c57ba3
child 32952 aeb1e44fbc19
     1.1 --- a/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fundef.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -37,12 +37,12 @@
     1.4  val simp_attribs = map (Attrib.internal o K)
     1.5      [Simplifier.simp_add,
     1.6       Code.add_default_eqn_attribute,
     1.7 -     Nitpick_Const_Simp_Thms.add,
     1.8 -     Quickcheck_RecFun_Simp_Thms.add]
     1.9 +     Nitpick_Const_Simps.add,
    1.10 +     Quickcheck_RecFun_Simps.add]
    1.11  
    1.12  val psimp_attribs = map (Attrib.internal o K)
    1.13      [Simplifier.simp_add,
    1.14 -     Nitpick_Const_Psimp_Thms.add]
    1.15 +     Nitpick_Const_Psimps.add]
    1.16  
    1.17  fun note_theorem ((name, atts), ths) =
    1.18    LocalTheory.note Thm.generatedK ((Binding.qualified_name name, atts), ths)
    1.19 @@ -202,7 +202,7 @@
    1.20      "declaration of congruence rule for function definitions"
    1.21    #> setup_case_cong
    1.22    #> FundefRelation.setup
    1.23 -  #> FundefCommon.TerminationSimps.setup
    1.24 +  #> FundefCommon.Termination_Simps.setup
    1.25  
    1.26  val get_congs = FundefCtxTree.get_fundef_congs
    1.27