src/HOL/Library/Eval.thy
changeset 25557 ea6b11021e79
parent 25536 01753a944433
child 25559 f14305fb698c
--- 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