# HG changeset patch # User lcp # Date 785633501 -3600 # Node ID 5207fca25b6b2fd53584dfd764362af7df5a3786 # Parent 584b3475e8599781f1700980a09e2efc31c6d45c ZF/Datatype/datatype_decl: supplies a SINGLE domain for the mutually recursive construction. This is [q]univ(A), which is closed under sum. diff -r 584b3475e859 -r 5207fca25b6b src/ZF/Datatype.ML --- a/src/ZF/Datatype.ML Thu Nov 24 00:31:08 1994 +0100 +++ b/src/ZF/Datatype.ML Thu Nov 24 00:31:41 1994 +0100 @@ -81,10 +81,9 @@ val big_rec_name = space_implode "_" rec_names and srec_tms = mk_list (map fst rec_pairs) and scons = mk_scons rec_pairs - and sdom = (*default domain?*) - if dom = "" then co ^ "data_domain rec_tms" - else "replicate " ^ string_of_int (length rec_names) ^ - " (readtm (sign_of thy) iT " ^ dom ^ ")" + and sdom_sum = + if dom = "" then co ^ "data_domain rec_tms" (*default*) + else "readtm (sign_of thy) iT " ^ dom val stri_name = big_rec_name ^ "_Intrnl" val con_names = flat (map (map (trim o #1 o #1) o snd) rec_pairs) in @@ -92,8 +91,10 @@ \structure " ^ stri_name ^ " =\n\ \ let open Ind_Syntax in\n\ \ struct\n\ + \ val _ = writeln \"" ^ co ^ + "Datatype definition " ^ big_rec_name ^ "\"\n\ \ val rec_tms\t= map (readtm (sign_of thy) iT) " ^ srec_tms ^ "\n\ - \ val domts\t= " ^ sdom ^ "\n\ + \ val dom_sum\t= " ^ sdom_sum ^ "\n\ \ and con_ty_lists\t= read_constructs (sign_of thy)\n" ^ scons ^ "\n\ \ val intr_tms\t= mk_all_intr_tms (rec_tms, con_ty_lists)\n\ @@ -104,12 +105,12 @@ stri_name ^ ".con_ty_lists) \n\ \ |> " ^ co ^ "Ind.add_fp_def_i \n (" ^ stri_name ^ ".rec_tms, " ^ - stri_name ^ ".domts, " ^ + stri_name ^ ".dom_sum, " ^ stri_name ^ ".intr_tms)" , "structure " ^ big_rec_name ^ " =\n\ \ struct\n\ - \ val _ = writeln \"" ^ co ^ + \ val _ = writeln \"Proofs for " ^ co ^ "Datatype definition " ^ big_rec_name ^ "\"\n\ \ structure Result = " ^ co ^ "Data_section_Fun\n\ \ (open " ^ stri_name ^ "\n\