# HG changeset patch
# User wenzelm
# Date 911383184 -3600
# Node ID b9d5f5901b59c748c9eb4f1524f385765e5732d0
# Parent  5a8c731b15328b90619bbcc9619f2d7312120d8c
'prop', 'term', 'typ';

diff -r 5a8c731b1532 -r b9d5f5901b59 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Nov 18 10:59:20 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Nov 18 10:59:44 1998 +0100
@@ -419,15 +419,15 @@
   OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);
 
 val print_propP =
-  OuterSyntax.parser true "print_prop" "read and print proposition"
+  OuterSyntax.parser true "prop" "read and print proposition"
     (term >> IsarCmd.print_prop);
 
 val print_termP =
-  OuterSyntax.parser true "print_term" "read and print term"
+  OuterSyntax.parser true "term" "read and print term"
     (term >> IsarCmd.print_term);
 
 val print_typeP =
-  OuterSyntax.parser true "print_type" "read and print type"
+  OuterSyntax.parser true "typ" "read and print type"
     (typ >> IsarCmd.print_type);