--- a/src/HOL/Nominal/nominal_package.ML Thu Jun 19 20:34:28 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Thu Jun 19 20:47:58 2008 +0200
@@ -116,11 +116,6 @@
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
-fun read_typ sign ((Ts, sorts), str) =
- let
- val T = Type.no_tvars (Sign.read_def_typ (sign, (AList.lookup op =)
- (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
- in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
(** simplification procedure for sorting permutations **)
@@ -2016,7 +2011,7 @@
thy13
end;
-val add_nominal_datatype = gen_add_nominal_datatype read_typ true;
+val add_nominal_datatype = gen_add_nominal_datatype DatatypePackage.read_typ true;
(* FIXME: The following stuff should be exported by DatatypePackage *)