proper ML interface set_full_types;
authorwenzelm
Wed, 24 Jun 2009 20:52:49 +0200
changeset 31793 7c10b13d49fe
parent 31792 d5a6096b94ad
child 31794 71af1fd6a5e4
proper ML interface set_full_types;
src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Wed Jun 24 17:50:49 2009 +0200
+++ b/src/HOL/Tools/atp_manager.ML	Wed Jun 24 20:52:49 2009 +0200
@@ -17,6 +17,7 @@
   val get_timeout: unit -> int
   val set_timeout: int -> unit
   val get_full_types: unit -> bool
+  val set_full_types: bool -> unit
   val kill: unit -> unit
   val info: unit -> unit
   val messages: int option -> unit
@@ -57,6 +58,7 @@
 fun set_timeout time = CRITICAL (fn () => timeout := time);
 
 fun get_full_types () = CRITICAL (fn () => ! full_types);
+fun set_full_types bool = CRITICAL (fn () => full_types := bool);
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_proof