src/HOL/Tools/primrec.ML
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;