src/HOL/Nominal/Nominal.thy
changeset 41562 90fb3d7474df
parent 41550 efa734d9b221
child 41798 c3aa3c87ef21
     1.1 --- a/src/HOL/Nominal/Nominal.thy	Sat Jan 15 12:35:29 2011 +0100
     1.2 +++ b/src/HOL/Nominal/Nominal.thy	Sat Jan 15 12:38:56 2011 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4    ("nominal_primrec.ML")
     1.5    ("nominal_inductive.ML")
     1.6    ("nominal_inductive2.ML")
     1.7 -  ("old_primrec.ML")
     1.8  begin 
     1.9  
    1.10  section {* Permutations *}
    1.11 @@ -3605,7 +3604,6 @@
    1.12  (***************************************)
    1.13  (* setup for the individial atom-kinds *)
    1.14  (* and nominal datatypes               *)
    1.15 -use "old_primrec.ML"
    1.16  use "nominal_atoms.ML"
    1.17  
    1.18  (************************************************************)