src/HOL/Tools/SMT2/smt2_failure.ML

     Out_Of_Memory |
     Abnormal_Termination of int |
     Other_Failure of string
   val string_of_failure: failure -> string
   exception SMT of failure
-end
+end;
 
 structure SMT2_Failure: SMT2_FAILURE =
 struct
 
 datatype failure =

       "Solver terminated abnormally with error code " ^ string_of_int err
   | string_of_failure (Other_Failure msg) = msg
 
 exception SMT of failure
 
-end
+end;