get-rulenames

Improving space efficiency of inductive/datatype definitions.
Reduce usage of "open" and change struct open X; D end to
let open X in struct D end end whenever possible -- removes X from the final
structure. Especially needed for functors Intr_elim and Indrule.

intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of
generating a new one. Inductive defs no longer export sumprod_free_SEs

ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM.
It is never used outside, is easily recovered using
bnd_mono and def_lfp_Tarski, and takes up considerable store.

Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items
no longer exported.

mutual_induct is simply "True" unless it is going to be
significantly different from induct -- either because there is mutual
recursion or because it involves tuples.

#!/bin/sh
#   Title: 	get-rulenames  (see also make-rulenames)
#   Author: 	Larry Paulson, Cambridge University Computer Laboratory
#   Copyright   1990  University of Cambridge
#
#shell script to generate "val" declarations for a theory's axioms 
#  also generates a comma-separated list of axiom names
#
#  usage:  make-rulenames  <file>
#
#Rule lines begin with a line containing the word "extend_theory"
#       and end   with a line containing the word "get_axiom"
#Each rule name xyz must appear on a line that begins
#        <spaces> ("xyz"
#Output lines have the form
#        val Eq_comp = ax"Eq_comp";
#
sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/val \1	= ax"\1";/p' $1
echo
echo `sed -n -e '/ext[end]*_theory/,/get_axiom/ s/^[ []*("\([^"]*\)".*$/\1/p' $1 | tr '\012' ','`