1.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 15:11:25 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Mon May 17 23:54:15 2010 +0200
     1.3 @@ -24,8 +24,6 @@
     1.4  open Nitpick_Nut
     1.5  open Nitpick
     1.6  
     1.7 -structure K = OuterKeyword and P = OuterParse
     1.8 -
     1.9  val auto = Unsynchronized.ref false;
    1.10  
    1.11  val _ =
    1.12 @@ -289,14 +287,14 @@
    1.13    extract_params (ProofContext.init_global thy) false (default_raw_params thy)
    1.14    o map (apsnd single)
    1.15  
    1.16 -val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
    1.17 +val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
    1.18  val parse_value =
    1.19 -  Scan.repeat1 (P.minus >> single
    1.20 -                || Scan.repeat1 (Scan.unless P.minus P.name)
    1.21 -                || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
    1.22 -val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
    1.23 +  Scan.repeat1 (Parse.minus >> single
    1.24 +                || Scan.repeat1 (Scan.unless Parse.minus Parse.name)
    1.25 +                || Parse.$$$ "," |-- Parse.number >> prefix "," >> single) >> flat
    1.26 +val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
    1.27  val parse_params =
    1.28 -  Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
    1.29 +  Scan.optional (Parse.$$$ "[" |-- Parse.list parse_param --| Parse.$$$ "]") []
    1.30  
    1.31  fun handle_exceptions ctxt f x =
    1.32    f x
    1.33 @@ -375,15 +373,15 @@
    1.34                                        |> sort_strings |> cat_lines)))))
    1.35  
    1.36  val parse_nitpick_command =
    1.37 -  (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
    1.38 +  (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
    1.39  val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
    1.40  
    1.41 -val _ = OuterSyntax.improper_command "nitpick"
    1.42 +val _ = Outer_Syntax.improper_command "nitpick"
    1.43              "try to find a counterexample for a given subgoal using Nitpick"
    1.44 -            K.diag parse_nitpick_command
    1.45 -val _ = OuterSyntax.command "nitpick_params"
    1.46 +            Keyword.diag parse_nitpick_command
    1.47 +val _ = Outer_Syntax.command "nitpick_params"
    1.48              "set and display the default parameters for Nitpick"
    1.49 -            K.thy_decl parse_nitpick_params_command
    1.50 +            Keyword.thy_decl parse_nitpick_params_command
    1.51  
    1.52  fun auto_nitpick state =
    1.53    if not (!auto) then (false, state) else pick_nits [] true 1 0 state