src/HOL/HOLCF/Tools/fixrec.ML
changeset 46909 3c73a121a387
parent 46895 de5cfda8b2de
child 46949 94aa7b81bcf6
     1.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 17:17:52 2012 +0000
     1.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue Mar 13 20:04:24 2012 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4  
     1.5      fun one_def (Free(n,_)) r =
     1.6            let val b = Long_Name.base_name n
     1.7 -          in ((Binding.name (b^"_def"), []), r) end
     1.8 +          in ((Binding.name (Thm.def_name b), []), r) end
     1.9        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"
    1.10      fun defs [] _ = []
    1.11        | defs (l::[]) r = [one_def l r]