src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

-(* Author: Lukas Bulwahn, TU Muenchen
-
-Auxilary functions for predicate compiler
+(*  Title:      HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
+    Author:     Lukas Bulwahn, TU Muenchen
+
+Auxilary functions for predicate compiler.
 *)
+
+(* FIXME proper signature *)
 
 structure Predicate_Compile_Aux =
 struct
 
 (* general syntactic functions *)

     val intro''''' = map_term thy (maps_premises split_conj) intro''''
   in
     intro'''''
   end
 
-
-
 end;