src/HOL/Tools/record_package.ML
changeset 9040 249c135057d7
parent 8720 840c75ab2a7f
child 9230 17ae63f82ad8
     1.1 --- a/src/HOL/Tools/record_package.ML	Tue Jun 06 20:31:43 2000 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Tue Jun 06 20:32:10 2000 +0200
     1.3 @@ -551,7 +551,7 @@
     1.4  
     1.5  (* field_definitions *)
     1.6  
     1.7 -fun field_definitions fields names zeta moreT more vars named_vars thy =
     1.8 +fun field_definitions fields names xs zeta moreT more vars named_vars thy =
     1.9    let
    1.10      val sign = Theory.sign_of thy;
    1.11      val base = Sign.base_name;
    1.12 @@ -632,8 +632,8 @@
    1.13      val surj_pairs = map (prove [DatatypePackage.induct_tac "p" 1]
    1.14        (map Thm.symmetric field_defs @ dest_convs)) surj_props;
    1.15  
    1.16 -    fun mk_split th = SplitPairedAll.rule (th RS eq_reflection);
    1.17 -    val field_splits = map mk_split surj_pairs;
    1.18 +    fun mk_split (x, th) = SplitPairedAll.rule_params x moreN (th RS eq_reflection);
    1.19 +    val field_splits = map2 mk_split (xs, surj_pairs);
    1.20  
    1.21      val thms_thy =
    1.22        defs_thy
    1.23 @@ -773,7 +773,7 @@
    1.24      val (fields_thy, field_simps, field_injects, field_splits) =
    1.25        thy
    1.26        |> Theory.add_path bname
    1.27 -      |> field_definitions fields names zeta moreT more vars named_vars;
    1.28 +      |> field_definitions fields names xs zeta moreT more vars named_vars;
    1.29  
    1.30      val named_splits = map2 (fn (c, th) => (suffix field_typeN c, th)) (names, field_splits);
    1.31