src/HOL/Tools/SMT2/smt2_systems.ML

     Z3_Non_Commercial_Unknown |
     Z3_Non_Commercial_Accepted |
     Z3_Non_Commercial_Declined
   val z3_non_commercial: unit -> z3_non_commercial
   val z3_extensions: bool Config.T
-end
+end;
 
 structure SMT2_Systems: SMT2_SYSTEMS =
 struct
 
 (* helper functions *)

 val _ = Theory.setup (
   SMT2_Solver.add_solver cvc3 #>
   SMT2_Solver.add_solver yices #>
   SMT2_Solver.add_solver z3)
 
-end
+end;