diff -r 8d3b7c27049b -r ea6b11021e79 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Thu Dec 06 12:58:01 2007 +0100
+++ b/src/HOL/Library/Eval.thy	Thu Dec 06 15:10:09 2007 +0100
@@ -151,7 +151,7 @@
       thy
       |> Instance.instantiate (tycos, sorts, @{sort term_of})
            (pair ()) ((K o K) (Class.intro_classes_tac []))
-      |> PrimrecPackage.gen_primrec thy_note thy_def "" defs
+      |> OldPrimrecPackage.gen_primrec thy_note thy_def "" defs
       |> snd
     | NONE => thy;
   in DatatypePackage.interpretation interpretator end