@@ -1059,7 +1059,7 @@ elabPE info fc caller r =
10591059
10601060 mkSpecialised ist specapp_in = do
10611061 let (specTy, specapp) = getSpecTy ist specapp_in
1062− let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
1062+ let (n, newnm, pats) = getSpecClause ist specapp
10631063 let undef = case lookupDef newnm (tt_ctxt ist) of
10641064 [] -> True
10651065 _ -> False
@@ -1074,10 +1074,12 @@ elabPE info fc caller r =
10741074 iLOG $ "PE definition type : " ++ (show specTy)
10751075 ++ "\n" ++ show opts
10761076 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
1077− (showImp Nothing True False lhs ++ " = " ++
1078− showImp Nothing True False rhs)
1077+ showSep "\n"
1078+ (map (\ (lhs, rhs) ->
1079+ (showImp Nothing True False lhs ++ " = " ++
1080+ showImp Nothing True False rhs)) pats)
10791081 elabType info defaultSyntax "" fc opts newnm specTy
1080− let def = [PClause fc newnm lhs [] rhs []]
1082+ let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
10811083 elabClauses info fc opts newnm def
10821084 logLvl 1 $ "Specialised " ++ show newnm)
10831085 -- if it doesn't work, just don't specialise. Could happen for lots