# HG changeset patch
# User wenzelm
# Date 967761194 -7200
# Node ID a126bc3b73762962b852d88da2bdcccdd1746ae8
# Parent  da698a96c4f32408b1266c95010981ed4449d262
'declare' made proper command;

diff -r da698a96c4f3 -r a126bc3b7376 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Sep 01 00:32:46 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Fri Sep 01 00:33:14 2000 +0200
@@ -197,7 +197,7 @@
     (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
 
 val declareP =
-  OuterSyntax.improper_command "declare" "declare theorems (improper)" K.thy_script
+  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
     (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));