--- a/src/HOL/Inductive.thy Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/Inductive.thy Tue Sep 18 07:36:38 2007 +0200
@@ -11,6 +11,7 @@
("Tools/inductive_package.ML")
("Tools/inductive_set_package.ML")
("Tools/inductive_realizer.ML")
+ "Tools/dseq.ML"
("Tools/inductive_codegen.ML")
("Tools/datatype_aux.ML")
("Tools/datatype_prop.ML")
--- a/src/HOL/IsaMakefile Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 18 07:36:38 2007 +0200
@@ -112,7 +112,8 @@
Tools/datatype_case.ML Tools/datatype_codegen.ML \
Tools/datatype_hooks.ML Tools/datatype_package.ML \
Tools/datatype_prop.ML Tools/datatype_realizer.ML \
- Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML \
+ Tools/datatype_rep_proofs.ML Tools/dseq.ML \
+ Tools/function_package/auto_term.ML \
Tools/function_package/context_tree.ML \
Tools/function_package/fundef_common.ML \
Tools/function_package/fundef_core.ML \
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/dseq.ML Tue Sep 18 07:36:38 2007 +0200
@@ -0,0 +1,56 @@
+(* Title: HOL/Tools/DSeq.ML
+ ID: $Id$
+ Author: Stefan Berghofer, TU Muenchen
+
+Sequences with recursion depth limit.
+*)
+
+structure DSeq =
+struct
+
+fun maps f s 0 = Seq.empty
+ | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
+
+fun map f s i = Seq.map f (s i);
+
+fun append s1 s2 i = Seq.append (s1 i) (s2 i);
+
+fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
+
+fun single x i = Seq.single x;
+
+fun empty i = Seq.empty;
+
+fun guard b = if b then single () else empty;
+
+fun of_list xs i = Seq.of_list xs;
+
+fun list_of s = Seq.list_of (s ~1);
+
+fun pull s = Seq.pull (s ~1);
+
+fun hd s = Seq.hd (s ~1);
+
+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);
--- a/src/HOL/Tools/inductive_codegen.ML Tue Sep 18 07:36:15 2007 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Sep 18 07:36:38 2007 +0200
@@ -698,54 +698,3 @@
Scan.option (Args.$$$ "params" |-- Args.colon |-- Args.nat) >> uncurry add);
end;
-
-
-(**** sequences with recursion depth limit ****)
-
-structure DSeq =
-struct
-
-fun maps f s 0 = Seq.empty
- | maps f s i = Seq.maps (fn a => f a i) (s (i - 1));
-
-fun map f s i = Seq.map f (s i);
-
-fun append s1 s2 i = Seq.append (s1 i) (s2 i);
-
-fun interleave s1 s2 i = Seq.interleave (s1 i, s2 i);
-
-fun single x i = Seq.single x;
-
-fun empty i = Seq.empty;
-
-fun of_list xs i = Seq.of_list xs;
-
-fun list_of s = Seq.list_of (s ~1);
-
-fun pull s = Seq.pull (s ~1);
-
-fun hd s = Seq.hd (s ~1);
-
-end;
-
-
-(**** combinators for code generated from inductive predicates ****)
-
-infix 5 :->;
-infix 3 ++;
-
-fun s :-> f = DSeq.maps f s;
-
-fun s1 ++ s2 = DSeq.append s1 s2;
-
-fun ?? b = if b then DSeq.single () else DSeq.empty;
-
-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);