'declare' made proper command;
authorwenzelm
Fri Sep 01 00:33:14 2000 +0200 (2000-09-01)
changeset 9776a126bc3b7376
parent 9775 da698a96c4f3
child 9777 232fb8886765
'declare' made proper command;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Sep 01 00:32:46 2000 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Sep 01 00:33:14 2000 +0200
     1.3 @@ -197,7 +197,7 @@
     1.4      (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
     1.5  
     1.6  val declareP =
     1.7 -  OuterSyntax.improper_command "declare" "declare theorems (improper)" K.thy_script
     1.8 +  OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
     1.9      (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));
    1.10  
    1.11