diff -r 72176ec5e031 -r 3bb9be510a9d src/HOL/Tools/SMT/smt_utils.ML
--- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Dec 15 08:39:24 2010 +0100
@@ -6,17 +6,18 @@
 
 signature SMT_UTILS =
 sig
+  (*basic combinators*)
   val repeat: ('a -> 'a option) -> 'a -> 'a
   val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
 
-  (* types *)
+  (*types*)
   val dest_funT: int -> typ -> typ list * typ
 
-  (* terms *)
+  (*terms*)
   val dest_conj: term -> term * term
   val dest_disj: term -> term * term
 
-  (* patterns and instantiations *)
+  (*patterns and instantiations*)
   val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
   val destT1: ctyp -> ctyp
   val destT2: ctyp -> ctyp
@@ -24,7 +25,7 @@
   val instT: ctyp -> ctyp * cterm -> cterm
   val instT': cterm -> ctyp * cterm -> cterm
 
-  (* certified terms *)
+  (*certified terms*)
   val certify: Proof.context -> term -> cterm
   val typ_of: cterm -> typ
   val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
@@ -35,7 +36,7 @@
   val dest_cprop: cterm -> cterm
   val mk_cequals: cterm -> cterm -> cterm
 
-  (* conversions *)
+  (*conversions*)
   val if_conv: (term -> bool) -> conv -> conv -> conv
   val if_true_conv: (term -> bool) -> conv -> conv
   val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
@@ -45,6 +46,8 @@
 structure SMT_Utils: SMT_UTILS =
 struct
 
+(* basic combinators *)
+
 fun repeat f =
   let fun rep x = (case f x of SOME y => rep y | NONE => x)
   in rep end