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