# HG changeset patch
# User wenzelm
# Date 986665130 -7200
# Node ID e9d5dc758f5e6a5f578aec7eb5da4af109c70c89
# Parent  be12c6f1ea75dd97ba9bf2bda6672e48e5cfae68
thm output: Attrib.local_thmss;

diff -r be12c6f1ea75 -r e9d5dc758f5e src/Pure/Isar/isar_output.ML
--- a/src/Pure/Isar/isar_output.ML	Sat Apr 07 19:38:01 2001 +0200
+++ b/src/Pure/Isar/isar_output.ML	Sat Apr 07 19:38:50 2001 +0200
@@ -310,7 +310,7 @@
 
 val _ = add_commands
  [("text", args (Scan.lift Args.name) (output_with (K pretty_text))),
-  ("thm", args Attrib.local_thms (output_with pretty_thm)),
+  ("thm", args Attrib.local_thmss (output_with pretty_thm)),
   ("prop", args Args.local_prop (output_with pretty_term)),
   ("term", args Args.local_term (output_with pretty_term)),
   ("typ", args Args.local_typ_no_norm (output_with pretty_typ)),