src/HOL/Tools/SMT/smt_translate.ML
changeset 41123 3bb9be510a9d
parent 41059 d2b1fc1b8e19
child 41127 2ea84c8535c6
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 08:39:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 08:39:24 2010 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature SMT_TRANSLATE =
     1.6  sig
     1.7 -  (* intermediate term structure *)
     1.8 +  (*intermediate term structure*)
     1.9    datatype squant = SForall | SExists
    1.10    datatype 'a spattern = SPat of 'a list | SNoPat of 'a list
    1.11    datatype sterm =
    1.12 @@ -15,7 +15,7 @@
    1.13      SLet of string * sterm * sterm |
    1.14      SQua of squant * string list * sterm spattern list * int option * sterm
    1.15  
    1.16 -  (* configuration options *)
    1.17 +  (*configuration options*)
    1.18    type prefixes = {sort_prefix: string, func_prefix: string}
    1.19    type sign = {
    1.20      header: string list,