src/Pure/Isar/isar_syn.ML
changeset 37216 3165bc303f66
parent 37198 3af985b10550
child 37861 e1f028a8c76a
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  Isar/Pure outer syntax.
     1.5  *)
     1.6  
     1.7 -structure IsarSyn: sig end =
     1.8 +structure Isar_Syn: sig end =
     1.9  struct
    1.10  
    1.11  (** keywords **)
    1.12 @@ -28,7 +28,7 @@
    1.13  
    1.14  val _ =
    1.15    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
    1.16 -    (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
    1.17 +    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
    1.18  
    1.19  val _ =
    1.20    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
    1.21 @@ -38,43 +38,43 @@
    1.22  
    1.23  (** markup commands **)
    1.24  
    1.25 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
    1.26 -  (Parse.doc_source >> IsarCmd.header_markup);
    1.27 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
    1.28 +  (Parse.doc_source >> Isar_Cmd.header_markup);
    1.29  
    1.30 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
    1.31 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.32 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
    1.33 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.34  
    1.35 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "section" "section heading"
    1.36 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.37 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
    1.38 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.39  
    1.40 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
    1.41 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.42 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
    1.43 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.44  
    1.45  val _ =
    1.46 -  Outer_Syntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
    1.47 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.48 +  Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
    1.49 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.50  
    1.51 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
    1.52 -  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.53 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
    1.54 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.55  
    1.56 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
    1.57 -  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
    1.58 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
    1.59 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    1.60  
    1.61 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
    1.62 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    1.63 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
    1.64 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
    1.65  
    1.66 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
    1.67 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    1.68 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
    1.69 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
    1.70  
    1.71 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
    1.72 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
    1.73 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
    1.74 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
    1.75  
    1.76 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
    1.77 -  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
    1.78 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
    1.79 +  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
    1.80  
    1.81 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "txt_raw"
    1.82 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
    1.83    "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
    1.84 -  (Parse.doc_source >> IsarCmd.proof_markup);
    1.85 +  (Parse.doc_source >> Isar_Cmd.proof_markup);
    1.86  
    1.87  
    1.88  
    1.89 @@ -185,7 +185,7 @@
    1.90    Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
    1.91      (Scan.repeat1 Parse_Spec.spec >>
    1.92        (Toplevel.theory o
    1.93 -        (IsarCmd.add_axioms o
    1.94 +        (Isar_Cmd.add_axioms o
    1.95            tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
    1.96  
    1.97  val opt_unchecked_overloaded =
    1.98 @@ -197,7 +197,7 @@
    1.99    Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
   1.100      (opt_unchecked_overloaded --
   1.101        Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
   1.102 -      >> (Toplevel.theory o IsarCmd.add_defs));
   1.103 +      >> (Toplevel.theory o Isar_Cmd.add_defs));
   1.104  
   1.105  
   1.106  (* old constdefs *)
   1.107 @@ -296,10 +296,10 @@
   1.108      ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
   1.109        (Toplevel.theory o uncurry hide));
   1.110  
   1.111 -val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
   1.112 -val _ = hide_names "hide_type" IsarCmd.hide_type "types";
   1.113 -val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
   1.114 -val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
   1.115 +val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
   1.116 +val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
   1.117 +val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
   1.118 +val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
   1.119  
   1.120  
   1.121  (* use ML text *)
   1.122 @@ -314,7 +314,7 @@
   1.123  val _ =
   1.124    Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
   1.125      (Parse.path >>
   1.126 -      (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
   1.127 +      (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
   1.128  
   1.129  val _ =
   1.130    Outer_Syntax.command "ML" "ML text within theory or local theory"
   1.131 @@ -331,19 +331,19 @@
   1.132  
   1.133  val _ =
   1.134    Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
   1.135 -    (Parse.ML_source >> IsarCmd.ml_diag true);
   1.136 +    (Parse.ML_source >> Isar_Cmd.ml_diag true);
   1.137  
   1.138  val _ =
   1.139    Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
   1.140 -    (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
   1.141 +    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
   1.142  
   1.143  val _ =
   1.144    Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
   1.145 -    (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
   1.146 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
   1.147  
   1.148  val _ =
   1.149    Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
   1.150 -    (Parse.ML_source >> IsarCmd.local_setup);
   1.151 +    (Parse.ML_source >> Isar_Cmd.local_setup);
   1.152  
   1.153  val _ =
   1.154    Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
   1.155 @@ -357,14 +357,14 @@
   1.156  
   1.157  val _ =
   1.158    Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
   1.159 -    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
   1.160 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
   1.161  
   1.162  val _ =
   1.163    Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
   1.164      (Parse.name --
   1.165        (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
   1.166        Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
   1.167 -    >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
   1.168 +    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
   1.169  
   1.170  
   1.171  (* translation functions *)
   1.172 @@ -374,27 +374,27 @@
   1.173  val _ =
   1.174    Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
   1.175      (Keyword.tag_ml Keyword.thy_decl)
   1.176 -    (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
   1.177 +    (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
   1.178  
   1.179  val _ =
   1.180    Outer_Syntax.command "parse_translation" "install parse translation functions"
   1.181      (Keyword.tag_ml Keyword.thy_decl)
   1.182 -    (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
   1.183 +    (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
   1.184  
   1.185  val _ =
   1.186    Outer_Syntax.command "print_translation" "install print translation functions"
   1.187      (Keyword.tag_ml Keyword.thy_decl)
   1.188 -    (trfun >> (Toplevel.theory o IsarCmd.print_translation));
   1.189 +    (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
   1.190  
   1.191  val _ =
   1.192    Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
   1.193      (Keyword.tag_ml Keyword.thy_decl)
   1.194 -    (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
   1.195 +    (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
   1.196  
   1.197  val _ =
   1.198    Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
   1.199      (Keyword.tag_ml Keyword.thy_decl)
   1.200 -    (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
   1.201 +    (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
   1.202  
   1.203  
   1.204  (* oracles *)
   1.205 @@ -402,7 +402,7 @@
   1.206  val _ =
   1.207    Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
   1.208      (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
   1.209 -      (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
   1.210 +      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
   1.211  
   1.212  
   1.213  (* local theories *)
   1.214 @@ -537,22 +537,22 @@
   1.215  val _ =
   1.216    Outer_Syntax.command "have" "state local goal"
   1.217      (Keyword.tag_proof Keyword.prf_goal)
   1.218 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   1.219 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
   1.220  
   1.221  val _ =
   1.222    Outer_Syntax.command "hence" "abbreviates \"then have\""
   1.223      (Keyword.tag_proof Keyword.prf_goal)
   1.224 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   1.225 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
   1.226  
   1.227  val _ =
   1.228    Outer_Syntax.command "show" "state local goal, solving current obligation"
   1.229      (Keyword.tag_proof Keyword.prf_asm_goal)
   1.230 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   1.231 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
   1.232  
   1.233  val _ =
   1.234    Outer_Syntax.command "thus" "abbreviates \"then show\""
   1.235      (Keyword.tag_proof Keyword.prf_asm_goal)
   1.236 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   1.237 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
   1.238  
   1.239  
   1.240  (* facts *)
   1.241 @@ -673,32 +673,32 @@
   1.242  val _ =
   1.243    Outer_Syntax.command "qed" "conclude (sub-)proof"
   1.244      (Keyword.tag_proof Keyword.qed_block)
   1.245 -    (Scan.option Method.parse >> IsarCmd.qed);
   1.246 +    (Scan.option Method.parse >> Isar_Cmd.qed);
   1.247  
   1.248  val _ =
   1.249    Outer_Syntax.command "by" "terminal backward proof"
   1.250      (Keyword.tag_proof Keyword.qed)
   1.251 -    (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
   1.252 +    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
   1.253  
   1.254  val _ =
   1.255    Outer_Syntax.command ".." "default proof"
   1.256      (Keyword.tag_proof Keyword.qed)
   1.257 -    (Scan.succeed IsarCmd.default_proof);
   1.258 +    (Scan.succeed Isar_Cmd.default_proof);
   1.259  
   1.260  val _ =
   1.261    Outer_Syntax.command "." "immediate proof"
   1.262      (Keyword.tag_proof Keyword.qed)
   1.263 -    (Scan.succeed IsarCmd.immediate_proof);
   1.264 +    (Scan.succeed Isar_Cmd.immediate_proof);
   1.265  
   1.266  val _ =
   1.267    Outer_Syntax.command "done" "done proof"
   1.268      (Keyword.tag_proof Keyword.qed)
   1.269 -    (Scan.succeed IsarCmd.done_proof);
   1.270 +    (Scan.succeed Isar_Cmd.done_proof);
   1.271  
   1.272  val _ =
   1.273    Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
   1.274      (Keyword.tag_proof Keyword.qed)
   1.275 -    (Scan.succeed IsarCmd.skip_proof);
   1.276 +    (Scan.succeed Isar_Cmd.skip_proof);
   1.277  
   1.278  val _ =
   1.279    Outer_Syntax.command "oops" "forget proof"
   1.280 @@ -796,7 +796,7 @@
   1.281  
   1.282  val _ =
   1.283    Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
   1.284 -    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
   1.285 +    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
   1.286  
   1.287  val _ =
   1.288    Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
   1.289 @@ -808,32 +808,32 @@
   1.290  
   1.291  val _ =
   1.292    Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
   1.293 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
   1.294 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
   1.295  
   1.296  val _ =
   1.297    Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
   1.298 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
   1.299 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
   1.300  
   1.301  val _ =
   1.302    Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
   1.303 -    Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
   1.304 +    Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
   1.305  
   1.306  val _ =
   1.307    Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
   1.308 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
   1.309 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
   1.310  
   1.311  val _ =
   1.312    Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
   1.313 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
   1.314 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
   1.315  
   1.316  val _ =
   1.317    Outer_Syntax.improper_command "print_theorems"
   1.318        "print theorems of local theory or proof context" Keyword.diag
   1.319 -    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
   1.320 +    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
   1.321  
   1.322  val _ =
   1.323    Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
   1.324 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
   1.325 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
   1.326  
   1.327  val _ =
   1.328    Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
   1.329 @@ -842,89 +842,89 @@
   1.330  
   1.331  val _ =
   1.332    Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
   1.333 -    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
   1.334 +    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
   1.335  
   1.336  val _ =
   1.337    Outer_Syntax.improper_command "print_interps"
   1.338      "print interpretations of locale for this theory" Keyword.diag
   1.339 -    (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
   1.340 +    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
   1.341  
   1.342  val _ =
   1.343    Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
   1.344 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
   1.345 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
   1.346  
   1.347  val _ =
   1.348    Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
   1.349 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
   1.350 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
   1.351  
   1.352  val _ =
   1.353    Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
   1.354 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
   1.355 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
   1.356  
   1.357  val _ =
   1.358    Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
   1.359 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
   1.360 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
   1.361  
   1.362  val _ =
   1.363    Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
   1.364 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
   1.365 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
   1.366  
   1.367  val _ =
   1.368    Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
   1.369 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   1.370 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
   1.371  
   1.372  val _ =
   1.373    Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
   1.374 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
   1.375 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
   1.376  
   1.377  val _ =
   1.378    Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
   1.379 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
   1.380 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
   1.381  
   1.382  val _ =
   1.383    Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
   1.384 -    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   1.385 +    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
   1.386  
   1.387  val _ =
   1.388    Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
   1.389 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
   1.390 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
   1.391  
   1.392  val _ =
   1.393    Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
   1.394 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
   1.395 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
   1.396  
   1.397  val _ =
   1.398    Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
   1.399 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
   1.400 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
   1.401  
   1.402  val _ =
   1.403    Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
   1.404 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   1.405 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
   1.406  
   1.407  val _ =
   1.408    Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
   1.409 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   1.410 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
   1.411  
   1.412  val _ =
   1.413    Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
   1.414      (opt_modes -- Scan.option Parse_Spec.xthms1
   1.415 -      >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   1.416 +      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
   1.417  
   1.418  val _ =
   1.419    Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
   1.420 -    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   1.421 +    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
   1.422  
   1.423  val _ =
   1.424    Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
   1.425 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
   1.426 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
   1.427  
   1.428  val _ =
   1.429    Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
   1.430 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
   1.431 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
   1.432  
   1.433  val _ =
   1.434    Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
   1.435 -    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
   1.436 +    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
   1.437  
   1.438  val _ =
   1.439    Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
   1.440 @@ -936,7 +936,7 @@
   1.441    Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
   1.442      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
   1.443         Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
   1.444 -         (Toplevel.no_timing oo IsarCmd.unused_thms));
   1.445 +         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
   1.446  
   1.447  
   1.448  
   1.449 @@ -944,54 +944,54 @@
   1.450  
   1.451  val _ =
   1.452    Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
   1.453 -    (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
   1.454 +    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
   1.455  
   1.456  val _ =
   1.457    Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
   1.458 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
   1.459 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
   1.460  
   1.461  val _ =
   1.462    Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
   1.463      (Parse.name >> (fn name =>
   1.464 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
   1.465 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
   1.466  
   1.467  val _ =
   1.468    Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
   1.469      (Parse.name >> (fn name =>
   1.470 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
   1.471 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
   1.472  
   1.473  val _ =
   1.474    Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
   1.475      (Parse.name >> (fn name =>
   1.476 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
   1.477 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
   1.478  
   1.479  val _ =
   1.480    Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
   1.481      Keyword.diag (Parse.name >> (fn name =>
   1.482 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
   1.483 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
   1.484  
   1.485  val _ =
   1.486    Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
   1.487 -    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
   1.488 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
   1.489  
   1.490  val _ =
   1.491    Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
   1.492 -    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
   1.493 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
   1.494  
   1.495  val opt_limits =
   1.496    Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
   1.497  
   1.498  val _ =
   1.499    Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
   1.500 -    (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
   1.501 +    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
   1.502  
   1.503  val _ =
   1.504    Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
   1.505 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
   1.506 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
   1.507  
   1.508  val _ =
   1.509    Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
   1.510 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
   1.511 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
   1.512  
   1.513  val _ =
   1.514    Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
   1.515 @@ -999,11 +999,11 @@
   1.516  
   1.517  val _ =
   1.518    Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
   1.519 -    (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
   1.520 +    (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
   1.521  
   1.522  val _ =
   1.523    Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
   1.524 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
   1.525 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
   1.526  
   1.527  end;
   1.528