src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 open Sledgehammer_Fact_Preprocessor
 open ATP_Manager
 open ATP_Systems
 open Sledgehammer_Fact_Minimizer
 
-structure K = OuterKeyword and P = OuterParse
-
 (** Proof method used in Isar proofs **)
 
 val neg_clausify_setup =
   Method.setup @{binding neg_clausify}
                (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
                "conversion of goal to negated conjecture clauses"
 
 (** Attribute for converting a theorem into clauses **)
 
 val parse_clausify_attribute : attribute context_parser =
-  Scan.lift OuterParse.nat
+  Scan.lift Parse.nat
   >> (fn i => Thm.rule_attribute (fn context => fn th =>
                   let val thy = Context.theory_of context in
                     Meson.make_meta_clause (nth (cnf_axiom thy th) i)
                   end))
 

                             | params =>
                               (map check_raw_param params;
                                params |> map string_for_raw_param
                                       |> sort_strings |> cat_lines)))))
 
-val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
-val parse_value = Scan.repeat1 P.xname
-val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
-val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 Parse.xname
+val parse_param = parse_key -- Scan.optional (Parse.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
 val parse_fact_refs =
-  Scan.repeat1 (Scan.unless (P.name -- Args.colon)
-                            (P.xname -- Scan.option Attrib.thm_sel)
+  Scan.repeat1 (Scan.unless (Parse.name -- Args.colon)
+                            (Parse.xname -- Scan.option Attrib.thm_sel)
                 >> (fn (name, interval) =>
                        Facts.Named ((name, Position.none), interval)))
 val parse_relevance_chunk =
   (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
   || (Args.del |-- Args.colon |-- parse_fact_refs

 val parse_relevance_override =
   Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
                               >> merge_relevance_overrides))
                 (add_to_relevance_override [])
 val parse_sledgehammer_command =
-  (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
-   -- Scan.option P.nat) #>> sledgehammer_trans
+  (Scan.optional Parse.short_ident runN -- parse_params -- parse_relevance_override
+   -- Scan.option Parse.nat) #>> sledgehammer_trans
 val parse_sledgehammer_params_command =
   parse_params #>> sledgehammer_params_trans
 
 val _ =
-  OuterSyntax.improper_command sledgehammerN
-      "search for first-order proof using automatic theorem provers" K.diag
+  Outer_Syntax.improper_command sledgehammerN
+      "search for first-order proof using automatic theorem provers" Keyword.diag
       parse_sledgehammer_command
 val _ =
-  OuterSyntax.command sledgehammer_paramsN
-      "set and display the default parameters for Sledgehammer" K.thy_decl
+  Outer_Syntax.command sledgehammer_paramsN
+      "set and display the default parameters for Sledgehammer" Keyword.thy_decl
       parse_sledgehammer_params_command
 
 val setup =
   neg_clausify_setup
   #> clausify_setup