src/Pure/Tools/find_theorems.ML
changeset 36950 75b8f26f2f07
parent 35625 9c818cab0dd0
child 36953 2af1ad9aa1a3
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -465,28 +465,27 @@
     1.4  
     1.5  local
     1.6  
     1.7 -structure P = OuterParse and K = OuterKeyword;
     1.8 -
     1.9  val criterion =
    1.10 -  P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> Name ||
    1.11 -  P.reserved "intro" >> K Intro ||
    1.12 -  P.reserved "introiff" >> K IntroIff ||
    1.13 -  P.reserved "elim" >> K Elim ||
    1.14 -  P.reserved "dest" >> K Dest ||
    1.15 -  P.reserved "solves" >> K Solves ||
    1.16 -  P.reserved "simp" |-- P.!!! (P.$$$ ":" |-- P.term) >> Simp ||
    1.17 -  P.term >> Pattern;
    1.18 +  Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
    1.19 +  Parse.reserved "intro" >> K Intro ||
    1.20 +  Parse.reserved "introiff" >> K IntroIff ||
    1.21 +  Parse.reserved "elim" >> K Elim ||
    1.22 +  Parse.reserved "dest" >> K Dest ||
    1.23 +  Parse.reserved "solves" >> K Solves ||
    1.24 +  Parse.reserved "simp" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.term) >> Simp ||
    1.25 +  Parse.term >> Pattern;
    1.26  
    1.27  val options =
    1.28    Scan.optional
    1.29 -    (P.$$$ "(" |--
    1.30 -      P.!!! (Scan.option P.nat -- Scan.optional (P.reserved "with_dups" >> K false) true
    1.31 -        --| P.$$$ ")")) (NONE, true);
    1.32 +    (Parse.$$$ "(" |--
    1.33 +      Parse.!!! (Scan.option Parse.nat -- Scan.optional (Parse.reserved "with_dups" >> K false) true
    1.34 +        --| Parse.$$$ ")")) (NONE, true);
    1.35  in
    1.36  
    1.37  val _ =
    1.38 -  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria" K.diag
    1.39 -    (options -- Scan.repeat (((Scan.option P.minus >> is_none) -- criterion))
    1.40 +  OuterSyntax.improper_command "find_theorems" "print theorems meeting specified criteria"
    1.41 +    Keyword.diag
    1.42 +    (options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
    1.43        >> (Toplevel.no_timing oo find_theorems_cmd));
    1.44  
    1.45  end;