src/HOL/Nominal/nominal_primrec.ML

 (*  Title:      HOL/Nominal/nominal_primrec.ML
     Author:     Norbert Voelker, FernUni Hagen
     Author:     Stefan Berghofer, TU Muenchen
 
 Package for defining functions on nominal datatypes by primitive recursion.
-Taken from HOL/Tools/primrec_package.ML
+Taken from HOL/Tools/primrec.ML
 *)
 
 signature NOMINAL_PRIMREC =
 sig
   val add_primrec: term list option -> term option ->

   end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)
 
-fun find_dts (dt_info : NominalPackage.nominal_datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : Nominal.nominal_datatype_info Symtab.table) _ [] = []
   | find_dts dt_info tnames' (tname::tnames) =
       (case Symtab.lookup dt_info tname of
           NONE => primrec_err (quote tname ^ " is not a nominal datatype")
         | SOME dt =>
             if tnames' subset (map (#1 o snd) (#descr dt)) then

     val fixes = List.take (fixes', length raw_fixes);
     val (names_atts, spec') = split_list spec;
     val eqns' = map unquantify spec'
     val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
       orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
-    val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
+    val dt_info = Nominal.get_nominal_datatypes (ProofContext.theory_of lthy);
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
       map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
     val _ =
       (if forall (curry eq_set lsrs) lsrss andalso forall
          (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>