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