src/Pure/Tools/find_consts.ML
changeset 33301 1fe9fc908ec3
parent 33158 6e3dc0ba2b06
child 35845 e5980f0ad025
--- a/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:26:47 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:56:02 2009 +0100
@@ -11,11 +11,10 @@
       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 *)
@@ -162,7 +161,7 @@
 
 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;