--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Oct 17 21:42:18 2015 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Sat Oct 17 22:31:21 2015 +0200
@@ -229,7 +229,7 @@
val dest_decl : (bool * binding option * string) parser =
@{keyword "("} |-- Scan.optional (@{keyword "lazy"} >> K true) false --
- (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ) --| @{keyword ")"} >> Parse.triple1
+ (Parse.binding >> SOME) -- (@{keyword "::"} |-- Parse.typ) --| @{keyword ")"} >> Scan.triple1
|| @{keyword "("} |-- @{keyword "lazy"} |-- Parse.typ --| @{keyword ")"}
>> (fn t => (true, NONE, t))
|| Parse.typ >> (fn t => (false, NONE, t))