src/HOL/Tools/SMT/smtlib_interface.ML

--- a/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:39:26 2010 +0200
+++ b/src/HOL/Tools/SMT/smtlib_interface.ML	Tue Oct 26 11:45:12 2010 +0200
@@ -15,7 +15,7 @@
   val add_builtins: builtins -> Context.generic -> Context.generic
   val add_logic: (term list -> string option) -> Context.generic ->
     Context.generic
-  val extra_norm: bool -> SMT_Normalize.extra_norm
+  val extra_norm: SMT_Normalize.extra_norm
   val interface: SMT_Solver.interface
 end
 
@@ -283,7 +283,7 @@
 (** interfaces **)
 
 val interface = {
-  extra_norm = extra_norm false,
+  extra_norm = extra_norm,
   translate = {
     prefixes = {
       sort_prefix = "S",