# HG changeset patch
# User haftmann
# Date 1342719519 -7200
# Node ID 828ace4f75ab06327c637a6d7033bdc9d0315fcd
# Parent  b6081af563a9470b8e4d5e883db0b083eb3d1244
removed ML module DSeq which was a part of the ancient code generator (cf. 58e33a125f32)

diff -r b6081af563a9 -r 828ace4f75ab src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Thu Jul 19 12:01:05 2012 +0200
+++ b/src/HOL/Inductive.thy	Thu Jul 19 19:38:39 2012 +0200
@@ -12,7 +12,6 @@
   "rep_datatype" :: thy_goal and
   "primrec" :: thy_decl
 uses
-  "Tools/dseq.ML"
   ("Tools/inductive.ML")
   ("Tools/Datatype/datatype_aux.ML")
   ("Tools/Datatype/datatype_prop.ML")
diff -r b6081af563a9 -r 828ace4f75ab src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 19 12:01:05 2012 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 19 19:38:39 2012 +0200
@@ -245,7 +245,6 @@
   Tools/abel_cancel.ML \
   Tools/arith_data.ML \
   Tools/cnf_funcs.ML \
-  Tools/dseq.ML \
   Tools/enriched_type.ML \
   Tools/inductive.ML \
   Tools/inductive_realizer.ML \
diff -r b6081af563a9 -r 828ace4f75ab src/HOL/Tools/dseq.ML
--- a/src/HOL/Tools/dseq.ML	Thu Jul 19 12:01:05 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,78 +0,0 @@
-(*  Title:      HOL/Tools/dseq.ML
-    Author:     Stefan Berghofer, TU Muenchen
-
-Sequences with recursion depth limit.
-*)
-
-signature DSEQ =
-sig
-  type 'a seq = int * int * int -> 'a Seq.seq;
-  val maps: ('a -> 'b seq) -> 'a seq -> 'b seq
-  val map: ('a -> 'b) -> 'a seq -> 'b seq
-  val append: 'a seq -> 'a seq -> 'a seq
-  val interleave: 'a seq -> 'a seq -> 'a seq
-  val single: 'a -> 'a seq
-  val empty: 'a seq
-  val guard: bool -> unit seq
-  val of_list: 'a list -> 'a seq
-  val list_of: 'a seq -> 'a list
-  val pull: 'a seq -> ('a * 'a Seq.seq) option
-  val hd: 'a seq -> 'a
-  val generator: (int -> 'a * 'b) -> 'a seq
-end;
-
-structure DSeq : DSEQ =
-struct
-
-type 'a seq = int * int * int -> 'a Seq.seq;
-
-fun maps f s (0, _, _) = Seq.empty
-  | maps f s (i, j, k) = Seq.maps (fn a => f a (i, j, k)) (s (i - 1, j, k));
-
-fun map f s p = Seq.map f (s p);
-
-fun append s1 s2 p = Seq.append (s1 p) (s2 p);
-
-fun interleave s1 s2 p = Seq.interleave (s1 p, s2 p);
-
-fun single x _ = Seq.single x;
-
-fun empty _ = Seq.empty;
-
-fun guard b = if b then single () else empty;
-
-fun of_list xs _ = Seq.of_list xs;
-
-fun list_of s = Seq.list_of (s (~1, 0, 0));
-
-fun pull s = Seq.pull (s (~1, 0, 0));
-
-fun hd s = Seq.hd (s (~1, 0, 0));
-
-fun generator g (i, 0, k) = Seq.empty
-  | generator g (i, j, k) =
-      Seq.make (fn () => SOME (fst (g k), generator g (i, j-1, k)));
-
-end;
-
-
-(* combinators for code generated from inductive predicates *)
-
-infix 5 :->;
-infix 3 ++;
-
-fun s :-> f = DSeq.maps f s;
-
-fun f ++ g = DSeq.append f g;
-
-val ?? = DSeq.guard;
-
-fun ??? f g = f o g;
-
-fun ?! s = is_some (DSeq.pull s);
-
-fun equal__1 x = DSeq.single x;
-
-val equal__2 = equal__1;
-
-fun equal__1_2 (x, y) = ?? (x = y);