diff -r b73b74fe23c3 -r 4fb8a33f74d6 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 12:06:17 2009 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Tue Oct 20 14:22:02 2009 +0200
@@ -8,17 +8,15 @@
 sig
   exception SMT_COUNTEREXAMPLE of bool * term list
 
-  datatype interface = Interface of {
+  type interface = {
     normalize: SMT_Normalize.config list,
     translate: SMT_Translate.config }
-
-  datatype proof_data = ProofData of {
+  type proof_data = {
     context: Proof.context,
     output: string list,
     recon: SMT_Translate.recon,
     assms: thm list option }
-
-  datatype solver_config = SolverConfig of {
+  type solver_config = {
     command: {env_var: string, remote_name: string},
     arguments: string list,
     interface: interface,
@@ -58,17 +56,17 @@
 exception SMT_COUNTEREXAMPLE of bool * term list
 
 
-datatype interface = Interface of {
+type interface = {
   normalize: SMT_Normalize.config list,
   translate: SMT_Translate.config }
 
-datatype proof_data = ProofData of {
+type proof_data = {
   context: Proof.context,
   output: string list,
   recon: SMT_Translate.recon,
   assms: thm list option }
 
-datatype solver_config = SolverConfig of {
+type solver_config = {
   command: {env_var: string, remote_name: string},
   arguments: string list,
   interface: interface,
@@ -144,12 +142,12 @@
 end
 
 fun make_proof_data ctxt ((recon, thms), ls) =
-  ProofData {context=ctxt, output=ls, recon=recon, assms=SOME thms}
+  {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
 fun gen_solver solver ctxt prems =
   let
-    val SolverConfig {command, arguments, interface, reconstruct} = solver ctxt
-    val Interface {normalize=nc, translate=tc} = interface
+    val {command, arguments, interface, reconstruct} = solver ctxt
+    val {normalize=nc, translate=tc} = interface
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize nc ctxt prems