changeset 38342 | 09d4a04d5c2e |
parent 37145 | 01aa36932739 |
child 38350 | 480b2de9927c |
--- a/src/HOL/Tools/primrec.ML Wed Aug 11 12:24:24 2010 +0200 +++ b/src/HOL/Tools/primrec.ML Wed Aug 11 12:30:48 2010 +0200 @@ -299,7 +299,7 @@ fun add_primrec_overloaded ops fixes specs thy = let - val lthy = Theory_Target.overloading ops thy; + val lthy = Overloading.overloading ops thy; val ((ts, simps), lthy') = add_primrec fixes specs lthy; val simps' = ProofContext.export lthy' lthy simps; in ((ts, simps'), Local_Theory.exit_global lthy') end;