src/Pure/Tools/find_consts.ML
changeset 33301 1fe9fc908ec3
parent 33158 6e3dc0ba2b06
child 35845 e5980f0ad025
     1.1 --- a/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:26:47 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Thu Oct 29 11:56:02 2009 +0100
     1.3 @@ -11,11 +11,10 @@
     1.4        Strict of string
     1.5      | Loose of string
     1.6      | Name of string
     1.7 -
     1.8    val find_consts : Proof.context -> (bool * criterion) list -> unit
     1.9  end;
    1.10  
    1.11 -structure FindConsts : FIND_CONSTS =
    1.12 +structure Find_Consts : FIND_CONSTS =
    1.13  struct
    1.14  
    1.15  (* search criteria *)
    1.16 @@ -162,7 +161,7 @@
    1.17  
    1.18  val _ =
    1.19    OuterSyntax.improper_command "find_consts" "search constants by type pattern" K.diag
    1.20 -    (Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.21 +    (Scan.repeat ((Scan.option P.minus >> is_none) -- criterion)
    1.22        >> (Toplevel.no_timing oo find_consts_cmd));
    1.23  
    1.24  end;