src/Pure/Isar/isar_syn.ML
changeset 22117 505e040bdcdb
parent 22088 4c53bb6e10e4
child 22202 0544af1a5117
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jan 19 22:08:25 2007 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 19 22:08:26 2007 +0100
     1.3 @@ -24,43 +24,43 @@
     1.4  
     1.5  (** markup commands **)
     1.6  
     1.7 -val headerP = OuterSyntax.markup_command IsarOutput.Markup "header" "theory header" K.diag
     1.8 +val headerP = OuterSyntax.markup_command ThyOutput.Markup "header" "theory header" K.diag
     1.9    (P.position P.text >> IsarCmd.add_header);
    1.10  
    1.11 -val chapterP = OuterSyntax.markup_command IsarOutput.Markup "chapter" "chapter heading"
    1.12 -  K.thy_heading (P.opt_locale_target -- P.position P.text >> IsarCmd.add_chapter);
    1.13 +val chapterP = OuterSyntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    1.14 +  K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_chapter);
    1.15  
    1.16 -val sectionP = OuterSyntax.markup_command IsarOutput.Markup "section" "section heading"
    1.17 -  K.thy_heading (P.opt_locale_target -- P.position P.text >> IsarCmd.add_section);
    1.18 +val sectionP = OuterSyntax.markup_command ThyOutput.Markup "section" "section heading"
    1.19 +  K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_section);
    1.20  
    1.21 -val subsectionP = OuterSyntax.markup_command IsarOutput.Markup "subsection" "subsection heading"
    1.22 -  K.thy_heading (P.opt_locale_target -- P.position P.text >> IsarCmd.add_subsection);
    1.23 +val subsectionP = OuterSyntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    1.24 +  K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsection);
    1.25  
    1.26  val subsubsectionP =
    1.27 -  OuterSyntax.markup_command IsarOutput.Markup "subsubsection" "subsubsection heading"
    1.28 -  K.thy_heading (P.opt_locale_target -- P.position P.text >> IsarCmd.add_subsubsection);
    1.29 +  OuterSyntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    1.30 +  K.thy_heading (P.opt_target -- P.position P.text >> IsarCmd.add_subsubsection);
    1.31  
    1.32 -val textP = OuterSyntax.markup_command IsarOutput.MarkupEnv "text" "formal comment (theory)"
    1.33 -  K.thy_decl (P.opt_locale_target -- P.position P.text >> IsarCmd.add_text);
    1.34 +val textP = OuterSyntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    1.35 +  K.thy_decl (P.opt_target -- P.position P.text >> IsarCmd.add_text);
    1.36  
    1.37 -val text_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "text_raw"
    1.38 +val text_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "text_raw"
    1.39    "raw document preparation text"
    1.40    K.thy_decl (P.position P.text >> IsarCmd.add_text_raw);
    1.41  
    1.42 -val sectP = OuterSyntax.markup_command IsarOutput.Markup "sect" "formal comment (proof)"
    1.43 +val sectP = OuterSyntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    1.44    (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_sect);
    1.45  
    1.46 -val subsectP = OuterSyntax.markup_command IsarOutput.Markup "subsect" "formal comment (proof)"
    1.47 +val subsectP = OuterSyntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    1.48    (K.tag_proof K.prf_heading) (P.position P.text >> IsarCmd.add_subsect);
    1.49  
    1.50 -val subsubsectP = OuterSyntax.markup_command IsarOutput.Markup "subsubsect"
    1.51 +val subsubsectP = OuterSyntax.markup_command ThyOutput.Markup "subsubsect"
    1.52    "formal comment (proof)" (K.tag_proof K.prf_heading)
    1.53    (P.position P.text >> IsarCmd.add_subsubsect);
    1.54  
    1.55 -val txtP = OuterSyntax.markup_command IsarOutput.MarkupEnv "txt" "formal comment (proof)"
    1.56 +val txtP = OuterSyntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    1.57    (K.tag_proof K.prf_decl) (P.position P.text >> IsarCmd.add_txt);
    1.58  
    1.59 -val txt_rawP = OuterSyntax.markup_command IsarOutput.Verbatim "txt_raw"
    1.60 +val txt_rawP = OuterSyntax.markup_command ThyOutput.Verbatim "txt_raw"
    1.61    "raw document preparation text (proof)" (K.tag_proof K.prf_decl)
    1.62    (P.position P.text >> IsarCmd.add_txt_raw);
    1.63  
    1.64 @@ -89,7 +89,7 @@
    1.65      (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
    1.66          P.!!! (P.list1 P.xname)) []
    1.67          -- Scan.optional (P.$$$ "(" |-- P.$$$ "attach" |-- Scan.repeat P.term --| P.$$$ ")") []
    1.68 -        -- Scan.repeat (P.thm_name ":" -- (P.prop >> single))
    1.69 +        -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
    1.70        >> (fn ((x, y), z) => Toplevel.theory (snd o AxClass.define_class x y z)));
    1.71  
    1.72  
    1.73 @@ -175,7 +175,7 @@
    1.74  
    1.75  val axiomsP =
    1.76    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
    1.77 -    (Scan.repeat1 P.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
    1.78 +    (Scan.repeat1 SpecParse.spec_name >> (Toplevel.theory o IsarCmd.add_axioms));
    1.79  
    1.80  val opt_unchecked_overloaded =
    1.81    Scan.optional (P.$$$ "(" |-- P.!!!
    1.82 @@ -184,7 +184,7 @@
    1.83  
    1.84  val defsP =
    1.85    OuterSyntax.command "defs" "define constants" K.thy_decl
    1.86 -    (opt_unchecked_overloaded -- Scan.repeat1 P.spec_name
    1.87 +    (opt_unchecked_overloaded -- Scan.repeat1 SpecParse.spec_name
    1.88        >> (Toplevel.theory o IsarCmd.add_defs));
    1.89  
    1.90  
    1.91 @@ -196,7 +196,7 @@
    1.92      --| Scan.option P.where_ >> P.triple1 ||
    1.93    P.name -- (P.mixfix >> pair NONE) --| Scan.option P.where_ >> P.triple2;
    1.94  
    1.95 -val old_constdef = Scan.option old_constdecl -- (P.opt_thm_name ":" -- P.prop);
    1.96 +val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
    1.97  
    1.98  val structs =
    1.99    Scan.optional ((P.$$$ "(" -- P.$$$ "structure") |-- P.!!! (P.simple_fixes --| P.$$$ ")")) [];
   1.100 @@ -215,22 +215,22 @@
   1.101        Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
   1.102    >> P.triple2;
   1.103  
   1.104 -val constdef = Scan.option constdecl -- (P.opt_thm_name ":" -- P.prop);
   1.105 +val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
   1.106  
   1.107  val definitionP =
   1.108    OuterSyntax.command "definition" "constant definition" K.thy_decl
   1.109 -    (P.opt_locale_target -- constdef
   1.110 +    (P.opt_target -- constdef
   1.111      >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
   1.112  
   1.113  val abbreviationP =
   1.114    OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
   1.115 -    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   1.116 +    (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop)
   1.117      >> (fn ((loc, mode), args) =>
   1.118          Toplevel.local_theory loc (Specification.abbreviation mode args)));
   1.119  
   1.120  val notationP =
   1.121    OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
   1.122 -    (P.opt_locale_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   1.123 +    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
   1.124      >> (fn ((loc, mode), args) =>
   1.125          Toplevel.local_theory loc (Specification.notation mode args)));
   1.126  
   1.127 @@ -239,15 +239,15 @@
   1.128  
   1.129  val axiomatizationP =
   1.130    OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl
   1.131 -    (P.opt_locale_target --
   1.132 +    (P.opt_target --
   1.133       (Scan.optional P.fixes [] --
   1.134 -      Scan.optional (P.where_ |-- P.!!! (P.and_list1 P.spec)) [])
   1.135 +      Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [])
   1.136      >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization x y)));
   1.137  
   1.138  
   1.139  (* theorems *)
   1.140  
   1.141 -fun theorems kind = P.opt_locale_target -- P.name_facts
   1.142 +fun theorems kind = P.opt_target -- SpecParse.name_facts
   1.143    >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
   1.144  
   1.145  val theoremsP =
   1.146 @@ -258,7 +258,7 @@
   1.147  
   1.148  val declareP =
   1.149    OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   1.150 -    (P.opt_locale_target -- (P.and_list1 P.xthms1 >> flat)
   1.151 +    (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat)
   1.152        >> (fn (loc, args) => Toplevel.local_theory loc
   1.153            (#2 o Specification.theorems "" [(("", []), args)])));
   1.154  
   1.155 @@ -299,7 +299,7 @@
   1.156  
   1.157  val setupP =
   1.158    OuterSyntax.command "setup" "apply ML theory setup" (K.tag_ml K.thy_decl)
   1.159 -    (Scan.option P.text >> (Toplevel.theory o PureThy.generic_setup));
   1.160 +    (Scan.option P.text >> (Toplevel.theory o IsarCmd.generic_setup));
   1.161  
   1.162  val method_setupP =
   1.163    OuterSyntax.command "method_setup" "define proof method in ML" (K.tag_ml K.thy_decl)
   1.164 @@ -308,7 +308,7 @@
   1.165  
   1.166  val declarationP =
   1.167    OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl)
   1.168 -    (P.opt_locale_target -- P.text
   1.169 +    (P.opt_target -- P.text
   1.170      >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt)));
   1.171  
   1.172  
   1.173 @@ -319,32 +319,32 @@
   1.174  val parse_ast_translationP =
   1.175    OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   1.176      (K.tag_ml K.thy_decl)
   1.177 -    (trfun >> (Toplevel.theory o Sign.parse_ast_translation));
   1.178 +    (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   1.179  
   1.180  val parse_translationP =
   1.181    OuterSyntax.command "parse_translation" "install parse translation functions"
   1.182      (K.tag_ml K.thy_decl)
   1.183 -    (trfun >> (Toplevel.theory o Sign.parse_translation));
   1.184 +    (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   1.185  
   1.186  val print_translationP =
   1.187    OuterSyntax.command "print_translation" "install print translation functions"
   1.188      (K.tag_ml K.thy_decl)
   1.189 -    (trfun >> (Toplevel.theory o Sign.print_translation));
   1.190 +    (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   1.191  
   1.192  val typed_print_translationP =
   1.193    OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   1.194      (K.tag_ml K.thy_decl)
   1.195 -    (trfun >> (Toplevel.theory o Sign.typed_print_translation));
   1.196 +    (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   1.197  
   1.198  val print_ast_translationP =
   1.199    OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   1.200      (K.tag_ml K.thy_decl)
   1.201 -    (trfun >> (Toplevel.theory o Sign.print_ast_translation));
   1.202 +    (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   1.203  
   1.204  val token_translationP =
   1.205    OuterSyntax.command "token_translation" "install token translation functions"
   1.206      (K.tag_ml K.thy_decl)
   1.207 -    (P.text >> (Toplevel.theory o Sign.token_translation));
   1.208 +    (P.text >> (Toplevel.theory o IsarCmd.token_translation));
   1.209  
   1.210  
   1.211  (* oracles *)
   1.212 @@ -352,7 +352,7 @@
   1.213  val oracleP =
   1.214    OuterSyntax.command "oracle" "declare oracle" (K.tag_ml K.thy_decl)
   1.215      (P.name -- (P.$$$ "(" |-- P.text --| P.$$$ ")" --| P.$$$ "=")
   1.216 -      -- P.text >> (Toplevel.theory o PureThy.add_oracle o P.triple1));
   1.217 +      -- P.text >> (Toplevel.theory o IsarCmd.oracle o P.triple1));
   1.218  
   1.219  
   1.220  (* local theories *)
   1.221 @@ -366,9 +366,9 @@
   1.222  (* locales *)
   1.223  
   1.224  val locale_val =
   1.225 -  (P.locale_expr --
   1.226 -    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 P.context_element)) [] ||
   1.227 -  Scan.repeat1 P.context_element >> pair Locale.empty);
   1.228 +  (SpecParse.locale_expr --
   1.229 +    Scan.optional (P.$$$ "+" |-- P.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   1.230 +  Scan.repeat1 SpecParse.context_element >> pair Locale.empty);
   1.231  
   1.232  val localeP =
   1.233    OuterSyntax.command "locale" "define named proof context" K.thy_decl
   1.234 @@ -382,17 +382,17 @@
   1.235  val interpretationP =
   1.236    OuterSyntax.command "interpretation"
   1.237      "prove and register interpretation of locale expression in theory or locale" K.thy_goal
   1.238 -    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! P.locale_expr
   1.239 +    (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! SpecParse.locale_expr
   1.240        >> (Toplevel.print oo (Toplevel.theory_to_proof o Locale.interpretation_in_locale I)) ||
   1.241 -      P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
   1.242 +      SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts >> (fn ((x, y), z) =>
   1.243          Toplevel.print o Toplevel.theory_to_proof (Locale.interpretation I x y z)));
   1.244  
   1.245  val interpretP =
   1.246    OuterSyntax.command "interpret"
   1.247      "prove and register interpretation of locale expression in proof context"
   1.248      (K.tag_proof K.prf_goal)
   1.249 -    (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts >> (fn ((x, y), z) =>
   1.250 -      Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
   1.251 +    (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts
   1.252 +      >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Locale.interpret Seq.single x y z)));
   1.253  
   1.254  
   1.255  
   1.256 @@ -402,9 +402,9 @@
   1.257  
   1.258  fun gen_theorem kind =
   1.259    OuterSyntax.command kind ("state " ^ kind) K.thy_goal
   1.260 -    (P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
   1.261 -      Scan.ahead (P.locale_keyword || P.statement_keyword)) ("", []) --
   1.262 -      P.general_statement >> (fn ((loc, a), (elems, concl)) =>
   1.263 +    (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   1.264 +      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) --
   1.265 +      SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) =>
   1.266        (Toplevel.print o
   1.267         Toplevel.local_theory_to_proof loc
   1.268           (Specification.theorem kind NONE (K I) a elems concl))));
   1.269 @@ -416,27 +416,27 @@
   1.270  val haveP =
   1.271    OuterSyntax.command "have" "state local goal"
   1.272      (K.tag_proof K.prf_goal)
   1.273 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   1.274 +    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   1.275  
   1.276  val henceP =
   1.277    OuterSyntax.command "hence" "abbreviates \"then have\""
   1.278      (K.tag_proof K.prf_goal)
   1.279 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   1.280 +    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   1.281  
   1.282  val showP =
   1.283    OuterSyntax.command "show" "state local goal, solving current obligation"
   1.284      (K.tag_proof K.prf_asm_goal)
   1.285 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   1.286 +    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   1.287  
   1.288  val thusP =
   1.289    OuterSyntax.command "thus" "abbreviates \"then show\""
   1.290      (K.tag_proof K.prf_asm_goal)
   1.291 -    (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   1.292 +    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   1.293  
   1.294  
   1.295  (* facts *)
   1.296  
   1.297 -val facts = P.and_list1 P.xthms1;
   1.298 +val facts = P.and_list1 SpecParse.xthms1;
   1.299  
   1.300  val thenP =
   1.301    OuterSyntax.command "then" "forward chaining"
   1.302 @@ -456,7 +456,7 @@
   1.303  val noteP =
   1.304    OuterSyntax.command "note" "define facts"
   1.305      (K.tag_proof K.prf_decl)
   1.306 -    (P.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   1.307 +    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss)));
   1.308  
   1.309  val usingP =
   1.310    OuterSyntax.command "using" "augment goal facts"
   1.311 @@ -479,25 +479,25 @@
   1.312  val assumeP =
   1.313    OuterSyntax.command "assume" "assume propositions"
   1.314      (K.tag_proof K.prf_asm)
   1.315 -    (P.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   1.316 +    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume)));
   1.317  
   1.318  val presumeP =
   1.319    OuterSyntax.command "presume" "assume propositions, to be established later"
   1.320      (K.tag_proof K.prf_asm)
   1.321 -    (P.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   1.322 +    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume)));
   1.323  
   1.324  val defP =
   1.325    OuterSyntax.command "def" "local definition"
   1.326      (K.tag_proof K.prf_asm)
   1.327      (P.and_list1
   1.328 -      (P.opt_thm_name ":" --
   1.329 +      (SpecParse.opt_thm_name ":" --
   1.330          ((P.name -- P.opt_mixfix) -- ((P.$$$ "\\<equiv>" || P.$$$ "==") |-- P.!!! P.termp)))
   1.331      >> (Toplevel.print oo (Toplevel.proof o Proof.def)));
   1.332  
   1.333  val obtainP =
   1.334    OuterSyntax.command "obtain" "generalized existence"
   1.335      (K.tag_proof K.prf_asm_goal)
   1.336 -    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- P.statement
   1.337 +    (P.parname -- Scan.optional (P.fixes --| P.where_) [] -- SpecParse.statement
   1.338        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain x y z)));
   1.339  
   1.340  val guessP =
   1.341 @@ -513,7 +513,7 @@
   1.342  
   1.343  val case_spec =
   1.344    (P.$$$ "(" |-- P.!!! (P.xname -- Scan.repeat1 (P.maybe P.name) --| P.$$$ ")") ||
   1.345 -    P.xname >> rpair []) -- P.opt_attribs >> P.triple1;
   1.346 +    P.xname >> rpair []) -- SpecParse.opt_attribs >> P.triple1;
   1.347  
   1.348  val caseP =
   1.349    OuterSyntax.command "case" "invoke local context"
   1.350 @@ -544,12 +544,12 @@
   1.351  val qedP =
   1.352    OuterSyntax.command "qed" "conclude (sub-)proof"
   1.353      (K.tag_proof K.qed_block)
   1.354 -    (Scan.option P.method >> (Toplevel.print3 oo IsarCmd.qed));
   1.355 +    (Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.qed));
   1.356  
   1.357  val terminal_proofP =
   1.358    OuterSyntax.command "by" "terminal backward proof"
   1.359      (K.tag_proof K.qed)
   1.360 -    (P.method -- Scan.option P.method >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   1.361 +    (Method.parse -- Scan.option Method.parse >> (Toplevel.print3 oo IsarCmd.terminal_proof));
   1.362  
   1.363  val default_proofP =
   1.364    OuterSyntax.command ".." "default proof"
   1.365 @@ -592,17 +592,17 @@
   1.366  val applyP =
   1.367    OuterSyntax.command "apply" "initial refinement step (unstructured)"
   1.368      (K.tag_proof K.prf_script)
   1.369 -    (P.method >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   1.370 +    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
   1.371  
   1.372  val apply_endP =
   1.373    OuterSyntax.command "apply_end" "terminal refinement (unstructured)"
   1.374      (K.tag_proof K.prf_script)
   1.375 -    (P.method >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   1.376 +    (Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
   1.377  
   1.378  val proofP =
   1.379    OuterSyntax.command "proof" "backward proof"
   1.380      (K.tag_proof K.prf_block)
   1.381 -    (Scan.option P.method >> (fn m => Toplevel.print o
   1.382 +    (Scan.option Method.parse >> (fn m => Toplevel.print o
   1.383        Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
   1.384        Toplevel.skip_proof (History.apply (fn i => i + 1))));
   1.385  
   1.386 @@ -610,7 +610,7 @@
   1.387  (* calculational proof commands *)
   1.388  
   1.389  val calc_args =
   1.390 -  Scan.option (P.$$$ "(" |-- P.!!! ((P.xthms1 --| P.$$$ ")")));
   1.391 +  Scan.option (P.$$$ "(" |-- P.!!! ((SpecParse.xthms1 --| P.$$$ ")")));
   1.392  
   1.393  val alsoP =
   1.394    OuterSyntax.command "also" "combine calculation and current facts"
   1.395 @@ -751,7 +751,7 @@
   1.396  
   1.397  val thm_depsP =
   1.398    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   1.399 -    K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   1.400 +    K.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   1.401  
   1.402  val criterion =
   1.403    P.reserved "name" |-- P.!!! (P.$$$ ":" |-- P.xname) >> FindTheorems.Name ||
   1.404 @@ -782,19 +782,19 @@
   1.405  
   1.406  val print_stmtsP =
   1.407    OuterSyntax.improper_command "print_statement" "print theorems as long statements" K.diag
   1.408 -    (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   1.409 +    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   1.410  
   1.411  val print_thmsP =
   1.412    OuterSyntax.improper_command "thm" "print theorems" K.diag
   1.413 -    (opt_modes -- P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   1.414 +    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   1.415  
   1.416  val print_prfsP =
   1.417    OuterSyntax.improper_command "prf" "print proof terms of theorems" K.diag
   1.418 -    (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   1.419 +    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   1.420  
   1.421  val print_full_prfsP =
   1.422    OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" K.diag
   1.423 -    (opt_modes -- Scan.option P.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   1.424 +    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   1.425  
   1.426  val print_propP =
   1.427    OuterSyntax.improper_command "prop" "read and print proposition" K.diag