tuned;
authorwenzelm
Thu Oct 12 22:57:35 2006 +0200 (2006-10-12 ago)
changeset 21004081674431d68
parent 21003 37492b0062c6
child 21005 8f3896f0e5af
tuned;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Oct 12 22:57:32 2006 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 12 22:57:35 2006 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  val endP =
     1.6    OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
     1.7 -    (Scan.succeed (Toplevel.exit o Toplevel.exit_local_theory));
     1.8 +    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
     1.9  
    1.10  val contextP =
    1.11    OuterSyntax.improper_command "context" "switch (local) theory context"
    1.12 @@ -748,9 +748,9 @@
    1.13    OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
    1.14      (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
    1.15  
    1.16 -val print_lthmsP =
    1.17 +val print_factsP =
    1.18    OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
    1.19 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms));
    1.20 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
    1.21  
    1.22  val print_casesP =
    1.23    OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
    1.24 @@ -919,11 +919,11 @@
    1.25    interpretationP, interpretP,
    1.26    (*diagnostic commands*)
    1.27    pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    1.28 -  print_syntaxP, print_theoremsP, print_localesP, print_localeP,
    1.29 -  print_registrationsP, print_attributesP, print_simpsetP,
    1.30 -  print_rulesP, print_induct_rulesP, print_trans_rulesP,
    1.31 -  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
    1.32 -  find_theoremsP, print_bindsP, print_lthmsP, print_casesP,
    1.33 +  print_syntaxP, print_factsP, print_theoremsP, print_localesP,
    1.34 +  print_localeP, print_registrationsP, print_attributesP,
    1.35 +  print_simpsetP, print_rulesP, print_induct_rulesP,
    1.36 +  print_trans_rulesP, print_methodsP, print_antiquotationsP,
    1.37 +  class_depsP, thm_depsP, find_theoremsP, print_bindsP, print_casesP,
    1.38    print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
    1.39    print_propP, print_termP, print_typeP,
    1.40    (*system commands*)