src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Nov 12 23:24:40 2012 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Nov 13 09:08:32 2012 +0100
@@ -6,6 +6,7 @@
 
 signature PREDICATE_COMPILE_CORE =
 sig
+  type seed = Random_Engine.seed
   type mode = Predicate_Compile_Aux.mode
   type options = Predicate_Compile_Aux.options
   type compilation = Predicate_Compile_Aux.compilation
@@ -23,18 +24,18 @@
   val print_all_modes : compilation -> Proof.context -> unit
 
   val put_pred_result : (unit -> term Predicate.pred) -> Proof.context -> Proof.context
-  val put_pred_random_result : (unit -> int * int -> term Predicate.pred * (int * int)) ->
+  val put_pred_random_result : (unit -> seed -> term Predicate.pred * seed) ->
     Proof.context -> Proof.context
   val put_dseq_result : (unit -> term DSequence.dseq) -> Proof.context -> Proof.context
-  val put_dseq_random_result : (unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)) ->
+  val put_dseq_random_result : (unit -> int -> int -> seed -> term DSequence.dseq * seed) ->
     Proof.context -> Proof.context
   val put_new_dseq_result : (unit -> int -> term Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_lseq_random_result :
-    (unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence) ->
+    (unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_lseq_random_stats_result :
-    (unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
+    (unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
 
   val code_pred_intro_attrib : attribute
@@ -70,6 +71,9 @@
 open Mode_Inference;
 open Predicate_Compile_Proof;
 
+type seed = Random_Engine.seed;
+
+
 (** fundamentals **)
 
 (* syntactic operations *)
@@ -1635,7 +1639,7 @@
 
 structure Pred_Random_Result = Proof_Data
 (
-  type T = unit -> int * int -> term Predicate.pred * (int * int)
+  type T = unit -> seed -> term Predicate.pred * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Pred_Random_Result"
 );
@@ -1651,7 +1655,7 @@
 
 structure Dseq_Random_Result = Proof_Data
 (
-  type T = unit -> int -> int -> int * int -> term DSequence.dseq * (int * int)
+  type T = unit -> int -> int -> seed -> term DSequence.dseq * seed
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Dseq_Random_Result"
 );
@@ -1667,7 +1671,7 @@
 
 structure Lseq_Random_Result = Proof_Data
 (
-  type T = unit -> int -> int -> int * int -> int -> term Lazy_Sequence.lazy_sequence
+  type T = unit -> int -> int -> seed -> int -> term Lazy_Sequence.lazy_sequence
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Random_Result"
 );
@@ -1675,7 +1679,7 @@
 
 structure Lseq_Random_Stats_Result = Proof_Data
 (
-  type T = unit -> int -> int -> int * int -> int -> (term * int) Lazy_Sequence.lazy_sequence
+  type T = unit -> int -> int -> seed -> int -> (term * int) Lazy_Sequence.lazy_sequence
   (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Lseq_Random_Stats_Result"
 );