# HG changeset patch # User wenzelm # Date 1245869569 -7200 # Node ID 7c10b13d49fea535df193fcfe02126ca143f5e2f # Parent d5a6096b94ade986781d0da1148b9d43ed58398e proper ML interface set_full_types; diff -r d5a6096b94ad -r 7c10b13d49fe 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