src/Pure/Isar/isar_syn.ML
changeset 21705 0f3ad56548bc
parent 21601 6588b947d631
child 21714 d64cb19c79e2
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Dec 07 21:08:48 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 07 21:08:50 2006 +0100
     1.3 @@ -219,12 +219,12 @@
     1.4  
     1.5  val definitionP =
     1.6    OuterSyntax.command "definition" "constant definition" K.thy_decl
     1.7 -    (P.opt_locale_target -- (constdef >> single)
     1.8 +    (P.opt_locale_target -- constdef
     1.9      >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition args)));
    1.10  
    1.11  val abbreviationP =
    1.12    OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl
    1.13 -    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop >> single)
    1.14 +    (P.opt_locale_target -- opt_mode -- (Scan.option constdecl -- P.prop)
    1.15      >> (fn ((loc, mode), args) =>
    1.16          Toplevel.local_theory loc (Specification.abbreviation mode args)));
    1.17