# HG changeset patch
# User wenzelm
# Date 963523064 -7200
# Node ID b54ebef48858328b5d35d3f23fce9fec5bd2d141
# Parent  b5bd2709a2c22f8af90703b07045b65f3bcfb6e0
defs: (overloaded) option;

diff -r b5bd2709a2c2 -r b54ebef48858 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Jul 13 23:17:14 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 13 23:17:44 2000 +0200
@@ -169,9 +169,13 @@
   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" K.thy_decl
     (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_axioms));
 
+val opt_overloaded =
+  Scan.optional (P.$$$ "(" |-- P.!!! ((P.$$$ "overloaded" >> K true) --| P.$$$ ")")) false;
+
 val defsP =
   OuterSyntax.command "defs" "define constants" K.thy_decl
-    (Scan.repeat1 (P.spec_name -- P.marg_comment) >> (Toplevel.theory o IsarThy.add_defs));
+    (opt_overloaded -- Scan.repeat1 (P.spec_name -- P.marg_comment)
+  >> (Toplevel.theory o IsarThy.add_defs));
 
 val constdefsP =
   OuterSyntax.command "constdefs" "declare and define constants" K.thy_decl
@@ -652,7 +656,7 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "binder", "concl",
-  "files", "in", "infixl", "infixr", "is", "output", "|"];
+  "files", "in", "infixl", "infixr", "is", "output", "overloaded", "|"];
 
 val parsers = [
   (*theory structure*)