@@ -529,13 +529,19 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
529529 (do hf <- un' env True bnames fx fy
530530 let ax' = hnormalise hf ctxt env (substNames hf ax)
531531 let ay' = hnormalise hf ctxt env (substNames hf ay)
532− ha <- un' env False bnames ax' ay'
532+ -- Don't normalise if we don't have to
533+ ha <- uplus (un' env False bnames (substNames hf ax)
534+ (substNames hf ay))
535+ (un' env False bnames ax' ay')
533536 sc 1
534537 combine env bnames hf ha)
535538 (do ha <- un' env False bnames ax ay
536539 let fx' = hnormalise ha ctxt env (substNames ha fx)
537540 let fy' = hnormalise ha ctxt env (substNames ha fy)
538− hf <- un' env False bnames fx' fy'
541+ -- Don't normalise if we don't have to
542+ hf <- uplus (un' env False bnames (substNames ha fx)
543+ (substNames ha fy))
544+ (un' env False bnames fx' fy')
539545 sc 1
540546 combine env bnames hf ha)
541547 | otherwise = unifyTmpFail appx appy
@@ -551,14 +557,6 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =
551557 = unifyFail appx appy
552558 checkHeads _ _ = return []
553559
554− unArgs as [] [] = return as
555− unArgs as (x : xs) (y : ys)
556− = do let x' = hnormalise as ctxt env (substNames as x)
557− let y' = hnormalise as ctxt env (substNames as y)
558− as' <- un' env False bnames x' y'
559− vs <- combine env bnames as as'
560− unArgs vs xs ys
561−
562560 numArgs tm = let (f, args) = unApply tm in length args
563561
564562 metavarApp tm = let (f, args) = unApply tm in