src/HOL/Tools/Sledgehammer/clausifier.ML
changeset 38282 319c59682c51
parent 38280 577f138af235
child 38608 01ed56c46259
--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 11:05:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 09 12:05:48 2010 +0200
@@ -100,7 +100,7 @@
 val [g_C,f_C] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_C}));
 val [f_S,g_S] = map (cterm_of @{theory}) (OldTerm.term_vars (prop_of @{thm abs_S}));
 
-(*FIXME: requires more use of cterm constructors*)
+(* FIXME: Requires more use of cterm constructors. *)
 fun abstract ct =
   let
       val thy = theory_of_cterm ct