Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/datatype_package.ML
changeset 13641 63d1790a43ed
parent 13480 bb72bd43c6c3
child 14174 f3cafd2929d5 
--- a/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Oct 10 14:26:50 2002 +0200
@@ -450,7 +450,8 @@
     val newTs = take (length (hd descr), recTs);
 
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
-      (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
+      (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
+        cargs) constrs) descr';
 
     (**** declare new types and constants ****)
 
@@ -470,9 +471,8 @@
           val Ts = map (typ_of_dtyp descr' sorts) cargs;
           val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
 
-          fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
-            | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
-               T --> nth_elem (k, rec_result_Ts);
+          fun mk_argT (dt, T) =
+            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
 
           val argTs = Ts @ map mk_argT recs
         in argTs ---> nth_elem (i, rec_result_Ts)
isabelle