@@ -207,10 +207,12 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
207 case val of
207 case val of
208 [(Function _ tm, Public)] ->
208 [(Function _ tm, Public)] ->
209 ev ntimes (n:stk) True env tm
209 ev ntimes (n:stk) True env tm
210+ [(Function _ tm, Hidden)] ->
211+ ev ntimes (n:stk) True env tm
210 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
212 [(TyDecl nt ty, _)] -> do vty <- ev ntimes stk True env ty
211 return $ VP nt n vty
213 return $ VP nt n vty
212 [(CaseOp ci _ _ _ cd, acc)]
214 [(CaseOp ci _ _ _ cd, acc)]
213− | acc == Public &&
215+ | (acc /= Frozen) &&
214 null (fst (cases_totcheck cd)) -> -- unoptimised version
216 null (fst (cases_totcheck cd)) -> -- unoptimised version
215 let (ns, tree) = getCases cd in
217 let (ns, tree) = getCases cd in
216 if blockSimplify ci n stk
218 if blockSimplify ci n stk
@@ -308,7 +310,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
308 do let val = lookupDefAcc n (spec || atRepl) ctxt
310 do let val = lookupDefAcc n (spec || atRepl) ctxt
309 case val of
311 case val of
310 [(CaseOp ci _ _ _ cd, acc)]
312 [(CaseOp ci _ _ _ cd, acc)]
311− | acc == Public -> -- unoptimised version
313+ | acc /= Frozen -> -- unoptimised version
312 let (ns, tree) = getCases cd in
314 let (ns, tree) = getCases cd in
313 if blockSimplify ci n stk
315 if blockSimplify ci n stk
314 then return $ unload env (VP Ref n ty) args
316 then return $ unload env (VP Ref n ty) args