--- a/src/HOL/Nominal/Nominal.thy Sat Jan 15 12:35:29 2011 +0100
+++ b/src/HOL/Nominal/Nominal.thy Sat Jan 15 12:38:56 2011 +0100
@@ -10,7 +10,6 @@
("nominal_primrec.ML")
("nominal_inductive.ML")
("nominal_inductive2.ML")
- ("old_primrec.ML")
begin
section {* Permutations *}
@@ -3605,7 +3604,6 @@
(***************************************)
(* setup for the individial atom-kinds *)
(* and nominal datatypes *)
-use "old_primrec.ML"
use "nominal_atoms.ML"
(************************************************************)