# HG changeset patch
# User paulson
# Date 820576010 -3600
# Node ID 439e1476a7f886d695c57966ed24575d874f5f64
# Parent  1f0009009219062d470f806e36905f9c2d668eff
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.

diff -r 1f0009009219 -r 439e1476a7f8 src/HOL/Inductive.ML
--- a/src/HOL/Inductive.ML	Mon Jan 01 11:54:36 1996 +0100
+++ b/src/HOL/Inductive.ML	Tue Jan 02 10:46:50 1996 +0100
@@ -12,11 +12,8 @@
 Products are used only to derive "streamlined" induction rules for relations
 *)
 
-local open Ind_Syntax
-in
-
 fun gen_fp_oper a (X,T,t) = 
-    let val setT = mk_setT T
+    let val setT = Ind_Syntax.mk_setT T
     in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
 
 structure Lfp_items =
@@ -33,19 +30,25 @@
   val induct	= def_Collect_coinduct
   end;
 
-end;
-
 
 functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
   : sig include INTR_ELIM INDRULE end =
-struct
-structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
-				    Fp=Lfp_items);
+let
+  structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
+					  Fp=Lfp_items);
 
-structure Indrule = Indrule_Fun
-    (structure Inductive=Inductive and Intr_elim=Intr_elim);
-
-open Intr_elim Indrule
+  structure Indrule = Indrule_Fun
+      (structure Inductive=Inductive and Intr_elim=Intr_elim);
+in 
+   struct 
+   val thy	= Intr_elim.thy
+   val defs	= Intr_elim.defs
+   val mono	= Intr_elim.mono
+   val intrs	= Intr_elim.intrs
+   val elim	= Intr_elim.elim
+   val mk_cases	= Intr_elim.mk_cases
+   open Indrule 
+   end
 end;
 
 
diff -r 1f0009009219 -r 439e1476a7f8 src/HOL/ind_syntax.ML
--- a/src/HOL/ind_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
+++ b/src/HOL/ind_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
@@ -121,4 +121,9 @@
 val refl_thin = prove_goal HOL.thy "!!P. [| a=a;  P |] ==> P"
      (fn _ => [assume_tac 1]);
 
+(*Includes rules for Suc and Pair since they are common constructions*)
+val elim_rls = [asm_rl, FalseE, Suc_neq_Zero, Zero_neq_Suc,
+		make_elim Suc_inject, 
+		refl_thin, conjE, exE, disjE];
+
 end;
diff -r 1f0009009219 -r 439e1476a7f8 src/HOL/thy_syntax.ML
--- a/src/HOL/thy_syntax.ML	Mon Jan 01 11:54:36 1996 +0100
+++ b/src/HOL/thy_syntax.ML	Tue Jan 02 10:46:50 1996 +0100
@@ -51,30 +51,34 @@
       in
          (";\n\n\
           \structure " ^ stri_name ^ " =\n\
-          \ let open Ind_Syntax in\n\
           \  struct\n\
           \  val _ = writeln \"" ^ co ^
                      "Inductive definition " ^ big_rec_name ^ "\"\n\
-          \  val rec_tms\t= map (readtm (sign_of thy) termTVar) "
+          \  val rec_tms\t= map (readtm (sign_of thy) Ind_Syntax.termTVar) "
                            ^ srec_tms ^ "\n\
           \  and intr_tms\t= map (readtm (sign_of thy) propT)\n"
                            ^ sintrs ^ "\n\
-          \  end\n\
-          \ end;\n\n\
+          \  end;\n\n\
           \val thy = thy |> " ^ co ^ "Ind.add_fp_def_i \n    (" ^
              stri_name ^ ".rec_tms, " ^
              stri_name ^ ".intr_tms)"
          ,
           "structure " ^ big_rec_name ^ " =\n\
-          \  struct\n\
+          \ let\n\
+          \  val _ = writeln \"Proofs for " ^ co ^ 
+                     "Inductive definition " ^ big_rec_name ^ "\"\n\
           \  structure Result = " ^ co ^ "Ind_section_Fun\n\
-          \  (open " ^ stri_name ^ "\n\
-          \   val thy\t\t= thy\n\
-          \   val monos\t\t= " ^ monos ^ "\n\
-          \   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
+          \\t  (open " ^ stri_name ^ "\n\
+          \\t   val thy\t\t= thy\n\
+          \\t   val monos\t\t= " ^ monos ^ "\n\
+          \\t   val con_defs\t\t= " ^ con_defs ^ ");\n\n\
+	  \ in\n\
+          \  struct\n\
           \  val " ^ mk_list (map mk_intr_name ipairs) ^ " = Result.intrs;\n\
           \  open Result\n\
-          \  end\n"
+          \  end\n\
+          \ end;\n\n\
+          \structure " ^ stri_name ^ " = struct end;\n\n"
          )
       end
     val ipairs = "intrs" $$-- repeat1 (ident -- !! string)