# HG changeset patch
# User paulson
# Date 820150620 -3600
# Node ID ecd90b82ab8eda279b79408d23dfbb3dabc1fcc5
# Parent  c60e9e1a1a23ac9cc9646b05a4718ef29ad6f4d2
Purely cosmetic changes

diff -r c60e9e1a1a23 -r ecd90b82ab8e src/ZF/intr_elim.ML
--- a/src/ZF/intr_elim.ML	Thu Dec 28 12:36:05 1995 +0100
+++ b/src/ZF/intr_elim.ML	Thu Dec 28 12:37:00 1995 +0100
@@ -31,7 +31,7 @@
   val dom_subset : thm			(*inclusion of recursive set in dom*)
   val intrs      : thm list		(*introduction rules*)
   val elim       : thm			(*case analysis theorem*)
-  val mk_cases : thm list -> string -> thm	(*generates case theorems*)
+  val mk_cases   : thm list -> string -> thm	(*generates case theorems*)
   end;
 
 signature INTR_ELIM_AUX =	(** Used to make induction rules **)
@@ -138,19 +138,15 @@
 
 in
   struct
-  val thy = Inductive.thy;
-
-  val defs = big_rec_def :: part_rec_defs;
-
-  val bnd_mono   = bnd_mono
+  val thy = Inductive.thy
+  and defs = big_rec_def :: part_rec_defs
+  and bnd_mono   = bnd_mono
   and dom_subset = dom_subset
   and intrs      = intrs;
 
   val elim = rule_by_tactic basic_elim_tac 
 		  (unfold RS Ind_Syntax.equals_CollectD);
 
-  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct);
-
   (*Applies freeness of the given constructors, which *must* be unfolded by
       the given defs.  Cannot simply use the local con_defs because  
       con_defs=[] for inference systems. 
@@ -161,7 +157,8 @@
 		      fold_tac defs)
 	(assume_read Inductive.thy s  RS  elim);
 
-  val rec_names = rec_names
+  val raw_induct = standard ([big_rec_def, bnd_mono] MRS Fp.induct)
+  and rec_names = rec_names
   end
 end;