src/HOL/Tools/refute.ML
changeset 14818 ad83019a66a4
parent 14810 4b4b97d29370
child 14965 7155b319eafa
     1.1 --- a/src/HOL/Tools/refute.ML	Sat May 29 14:55:56 2004 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat May 29 14:57:39 2004 +0200
     1.3 @@ -59,6 +59,9 @@
     1.4  structure Refute : REFUTE =
     1.5  struct
     1.6  
     1.7 +	(* FIXME comptibility -- should avoid std_output altogether *)
     1.8 +	val std_output = Output.std_output o Output.output;
     1.9 +
    1.10  	open PropLogic;
    1.11  
    1.12  	(* We use 'REFUTE' only for internal error conditions that should    *)