src/HOL/Inductive.ML
changeset 1430 439e1476a7f8
parent 923 ff1574a81019
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/Inductive.ML	Mon Jan 01 11:54:36 1996 +0100
     1.2 +++ b/src/HOL/Inductive.ML	Tue Jan 02 10:46:50 1996 +0100
     1.3 @@ -12,11 +12,8 @@
     1.4  Products are used only to derive "streamlined" induction rules for relations
     1.5  *)
     1.6  
     1.7 -local open Ind_Syntax
     1.8 -in
     1.9 -
    1.10  fun gen_fp_oper a (X,T,t) = 
    1.11 -    let val setT = mk_setT T
    1.12 +    let val setT = Ind_Syntax.mk_setT T
    1.13      in Const(a, (setT-->setT)-->setT) $ absfree(X, setT, t)  end;
    1.14  
    1.15  structure Lfp_items =
    1.16 @@ -33,19 +30,25 @@
    1.17    val induct	= def_Collect_coinduct
    1.18    end;
    1.19  
    1.20 -end;
    1.21 -
    1.22  
    1.23  functor Ind_section_Fun (Inductive: sig include INDUCTIVE_ARG INDUCTIVE_I end) 
    1.24    : sig include INTR_ELIM INDRULE end =
    1.25 -struct
    1.26 -structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
    1.27 -				    Fp=Lfp_items);
    1.28 +let
    1.29 +  structure Intr_elim = Intr_elim_Fun(structure Inductive=Inductive and 
    1.30 +					  Fp=Lfp_items);
    1.31  
    1.32 -structure Indrule = Indrule_Fun
    1.33 -    (structure Inductive=Inductive and Intr_elim=Intr_elim);
    1.34 -
    1.35 -open Intr_elim Indrule
    1.36 +  structure Indrule = Indrule_Fun
    1.37 +      (structure Inductive=Inductive and Intr_elim=Intr_elim);
    1.38 +in 
    1.39 +   struct 
    1.40 +   val thy	= Intr_elim.thy
    1.41 +   val defs	= Intr_elim.defs
    1.42 +   val mono	= Intr_elim.mono
    1.43 +   val intrs	= Intr_elim.intrs
    1.44 +   val elim	= Intr_elim.elim
    1.45 +   val mk_cases	= Intr_elim.mk_cases
    1.46 +   open Indrule 
    1.47 +   end
    1.48  end;
    1.49  
    1.50