Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.2); Thu, 15 Oct 1992 21:44:10 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28518; Thu, 15 Oct 92 13:27:19 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA28513; Thu, 15 Oct 92 13:27:06 -0700 Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 5.61d+YP/3.21) id AA17039; Thu, 15 Oct 92 13:26:13 -0700 Message-Id: <9210152026.AA17039@maui.cs.ucla.edu> To: info-hol@edu.uidaho.cs.ted Cc: chou@edu.ucla.cs Subject: 'definitions' takes a long time! Date: Thu, 15 Oct 92 13:26:11 PDT From: chou@edu.ucla.cs Is it normal that the ML function 'definitions' takes a long time when some definitions are very long? I have a theory one of whose definitions is more than a page long and another theory which have more definitions but they are all rather short. I found that 'definitions' takes a much longer time to retrieve the definitions in the former than in the latter. Is this to be expected? Any way to speed up 'definitions'? - Ching Tsun