Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <06795-0@swan.cl.cam.ac.uk>; Thu, 9 Jul 1992 10:15:23 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA07214;
          Thu, 9 Jul 92 00:06:34 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Received: from Maui.CS.UCLA.EDU by ted.cs.uidaho.edu (16.6/1.34) id AA07209;
          Thu, 9 Jul 92 00:06:28 -0700
Received: from LocalHost.cs.ucla.edu 
          by maui.cs.ucla.edu (Sendmail 5.61c+YP/3.19) id AA15751;
          Thu, 9 Jul 92 00:07:28 -0700
Message-Id: <9207090707.AA15751@maui.cs.ucla.edu>
To: info-hol@edu.uidaho.cs.ted
Subject: Binders
Date: Thu, 09 Jul 92 00:07:26 PDT
From: chou@edu.ucla.cs

I found out that if I define a binder B in theory `foo`, create a new
theory `goo`, and make `foo` a new_parent of `goo`, then B won't parse
as a binder in `goo`.  I would have to do:

    activate_binders `foo`

to activate the binder parsing.  Why is this necessary?  And what is
the difference between activate_binders and activate_all_binders?

- Ching Tsun