@@ -805,7 +805,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where
805805 (ns', (x',y',env',err', um) : ps')
806806
807807-- attempt to solve remaining problems with match_unify
808−matchProblems all ctxt ps inj holes = up [] ps where
808+matchProblems all ns ctxt ps inj holes = up ns ps where
809809 up ns [] = (ns, [])
810810 up ns ((x, y, env, err, um) : ps)
811811 | all || um == Match =
@@ -860,15 +860,19 @@ processTactic UnifyProblems ps
860860 notunified = updateNotunified ns' (notunified ps),
861861 holes = holes ps \\ (map fst ns') }, plog ps)
862862processTactic (MatchProblems all) ps
863− = let (ns', probs') = matchProblems all (context ps)
863+ = let (ns', probs') = matchProblems all [] (context ps)
864864 (problems ps)
865865 (injective ps)
866866 (holes ps)
867− pterm' = updateSolved ns' (pterm ps) in
868− return (ps { pterm = pterm', solved = Nothing, problems = probs',
867+ (ns'', probs'') = matchProblems all ns' (context ps)
868+ probs'
869+ (injective ps)
870+ (holes ps)
871+ pterm' = updateSolved ns'' (pterm ps) in
872+ return (ps { pterm = pterm', solved = Nothing, problems = probs'',
869873 previous = Just ps, plog = "",
870− notunified = updateNotunified ns' (notunified ps),
871− holes = holes ps \\ (map fst ns') }, plog ps)
874+ notunified = updateNotunified ns'' (notunified ps),
875+ holes = holes ps \\ (map fst ns'') }, plog ps)
872876processTactic t ps
873877 = case holes ps of
874878 [] -> fail "Nothing to fill in."