--- a/src/Pure/Syntax/parser.ML Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/Syntax/parser.ML Fri Jul 01 22:35:41 2005 +0200
@@ -627,7 +627,7 @@
(*Add parse tree to list and eliminate duplicates
saving the maximum precedence*)
-fun conc (t, prec:int) [] = (NONE, [(t, prec)])
+fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)])
| conc (t, prec) ((t', prec') :: ts) =
if t = t' then
(SOME prec', if prec' >= prec then (t', prec') :: ts
@@ -637,7 +637,7 @@
in (n, (t', prec') :: ts') end;
(*Update entry in used*)
-fun update_trees ((B, (i, ts)) :: used) (A, t) =
+fun update_trees ((B: nt_tag, (i, ts)) :: used) (A, t) =
if A = B then
let val (n, ts') = conc t ts
in ((A, (i, ts')) :: used, n) end
@@ -646,7 +646,7 @@
in ((B, (i, ts)) :: used', n) end;
(*Replace entry in used*)
-fun update_prec (A, prec) used =
+fun update_prec (A: nt_tag, prec) used =
let fun update ((hd as (B, (_, ts))) :: used, used') =
if A = B
then used' @ ((A, (prec, ts)) :: used)