src/Pure/Tools/find_consts.ML

 sig
   datatype criterion =
       Strict of string
     | Loose of string
     | Name of string
-
   val find_consts : Proof.context -> (bool * criterion) list -> unit
 end;
 
-structure FindConsts : FIND_CONSTS =
+structure Find_Consts : FIND_CONSTS =
 struct
 
 (* search criteria *)
 
 datatype criterion =

 
 in
 
 val _ =
   OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
-    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
+    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
       >> (Toplevel.no_timing oo find_consts_cmd));
 
 end;
 
 end;