# HG changeset patch
# User wenzelm
# Date 1160686655 -7200
# Node ID 081674431d683fc0e1d971dbcef34fce031c91f4
# Parent  37492b0062c676ef662324409a8e775416ebd862
tuned;

diff -r 37492b0062c6 -r 081674431d68 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 12 22:57:32 2006 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 12 22:57:35 2006 +0200
@@ -19,7 +19,7 @@
 
 val endP =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
-    (Scan.succeed (Toplevel.exit o Toplevel.exit_local_theory));
+    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
 
 val contextP =
   OuterSyntax.improper_command "context" "switch (local) theory context"
@@ -748,9 +748,9 @@
   OuterSyntax.improper_command "print_binds" "print term bindings of proof context" K.diag
     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
 
-val print_lthmsP =
+val print_factsP =
   OuterSyntax.improper_command "print_facts" "print facts of proof context" K.diag
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_lthms));
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
 
 val print_casesP =
   OuterSyntax.improper_command "print_cases" "print cases of proof context" K.diag
@@ -919,11 +919,11 @@
   interpretationP, interpretP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
-  print_syntaxP, print_theoremsP, print_localesP, print_localeP,
-  print_registrationsP, print_attributesP, print_simpsetP,
-  print_rulesP, print_induct_rulesP, print_trans_rulesP,
-  print_methodsP, print_antiquotationsP, class_depsP, thm_depsP,
-  find_theoremsP, print_bindsP, print_lthmsP, print_casesP,
+  print_syntaxP, print_factsP, print_theoremsP, print_localesP,
+  print_localeP, print_registrationsP, print_attributesP,
+  print_simpsetP, print_rulesP, print_induct_rulesP,
+  print_trans_rulesP, print_methodsP, print_antiquotationsP,
+  class_depsP, thm_depsP, find_theoremsP, print_bindsP, print_casesP,
   print_stmtsP, print_thmsP, print_prfsP, print_full_prfsP,
   print_propP, print_termP, print_typeP,
   (*system commands*)