--- a/src/HOL/Nominal/Nominal.thy Tue Sep 28 15:39:59 2010 +0200
+++ b/src/HOL/Nominal/Nominal.thy Wed Sep 29 09:07:58 2010 +0200
@@ -10,6 +10,7 @@
("nominal_primrec.ML")
("nominal_inductive.ML")
("nominal_inductive2.ML")
+ ("old_primrec.ML")
begin
section {* Permutations *}
@@ -3604,6 +3605,7 @@
(***************************************)
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
+use "old_primrec.ML"
use "nominal_atoms.ML"
(************************************************************)