removed duplicate of DatatypePackage.read_typ;
authorwenzelm
Thu, 19 Jun 2008 20:47:58 +0200
changeset 27275 f54aa7c4ff32
parent 27274 1c97c471db82
child 27276 ea82bd1e3c20
removed duplicate of DatatypePackage.read_typ;
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 *)