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;
```