src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 15 17:53:28 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 15 17:54:58 1999 +0200
@@ -463,7 +463,7 @@
     (Scan.succeed IsarCmd.print_lthms);
 
 val print_thmsP =
-  OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthm >> IsarCmd.print_thms);
+  OuterSyntax.improper_command "thm" "print theorems" K.diag (P.xthms1 >> IsarCmd.print_thms);
 
 val print_propP =
   OuterSyntax.improper_command "prop" "read and print proposition" K.diag