--- a/src/Pure/Isar/isar_syn.ML Sun Jul 30 12:51:33 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML Sun Jul 30 12:52:13 2000 +0200
@@ -340,9 +340,8 @@
val defP =
OuterSyntax.command "def" "local definition" K.prf_asm
- ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
- (P.$$$ "==" |-- P.termp)) >> P.triple1) -- P.marg_comment
- >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
+ ((P.opt_thm_name ":" -- (P.name -- (P.$$$ "==" |-- P.!!! P.termp)) >> P.triple1)
+ -- P.marg_comment >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
val fixP =
OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm