Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
def: no constraint on var;
authorwenzelm
Sun, 30 Jul 2000 12:52:13 +0200
changeset 9465 b285b91cd2b2
parent 9464 e290583864e4
child 9466 e9f5768bb656
def: no constraint on var;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle