# HG changeset patch
# User wenzelm
# Date 1213901278 -7200
# Node ID f54aa7c4ff32646e0d725ed860f46861344604f0
# Parent  1c97c471db82738c13f234328b44cd48cfe277d8
removed duplicate of DatatypePackage.read_typ;

diff -r 1c97c471db82 -r f54aa7c4ff32 src/HOL/Nominal/nominal_package.ML
--- 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 *)