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/datatype_codegen.ML
changeset 31737 b3f63611784e
parent 31723 f5cafe803b55 
--- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 08:38:57 2009 +0200
+++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Sun Jun 21 08:38:58 2009 +0200
@@ -6,7 +6,7 @@
 
 signature DATATYPE_CODEGEN =
 sig
-  val find_shortest_path: DatatypeAux.descr -> int -> (string * int) option
+  val find_shortest_path: Datatype.descr -> int -> (string * int) option
   val mk_eq_eqns: theory -> string -> (thm * bool) list
   val mk_case_cert: theory -> string -> thm
   val setup: theory -> theory
@@ -17,7 +17,7 @@
 
 (** find shortest path to constructor with no recursive arguments **)
 
-fun find_nonempty (descr: DatatypeAux.descr) is i =
+fun find_nonempty (descr: Datatype.descr) is i =
   let
     val (_, _, constrs) = the (AList.lookup (op =) descr i);
     fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
@@ -42,7 +42,7 @@
 
 (* datatype definition *)
 
-fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
+fun add_dt_defs thy defs dep module (descr: Datatype.descr) sorts gr =
   let
     val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
     val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
isabelle