--- a/src/HOL/Nominal/nominal_primrec.ML Fri Jul 03 16:51:56 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Jul 03 23:29:03 2009 +0200
@@ -223,7 +223,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : Nominal.nominal_datatype_info Symtab.table) _ [] = []
+fun find_dts (dt_info : NominalDatatype.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")
@@ -247,7 +247,7 @@
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 = Nominal.get_nominal_datatypes (ProofContext.theory_of lthy);
+ val dt_info = NominalDatatype.get_nominal_datatypes (ProofContext.theory_of lthy);
val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
val _ =