src/HOL/Tools/Function/fundef_common.ML
changeset 31902 862ae16a799d
parent 31775 2b04504fcb69
child 32603 e08fdd615333
     1.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 17:33:36 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Thu Jul 02 17:34:14 2009 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4  
     1.5  (* Simp rules for termination proofs *)
     1.6  
     1.7 -structure TerminationSimps = NamedThmsFun
     1.8 +structure Termination_Simps = Named_Thms
     1.9  (
    1.10    val name = "termination_simp" 
    1.11    val description = "Simplification rule for termination proofs"