src/HOL/Tools/datatype_rep_proofs.ML
changeset 7293 959e060f4a2f
parent 7257 745cfc8871e2
child 7499 23e090051cb8
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 18:36:41 1999 +0200
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 19:00:42 1999 +0200
     1.3 @@ -47,16 +47,16 @@
     1.4      val Datatype_thy = theory "Datatype";
     1.5      val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
     1.6      val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
     1.7 -      Funs_name, o_name] =
     1.8 +      Funs_name, o_name, sum_case_name] =
     1.9        map (Sign.intern_const (Theory.sign_of Datatype_thy))
    1.10 -        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
    1.11 +        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"];
    1.12  
    1.13      val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
    1.14           In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
    1.15 -         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
    1.16 +         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
    1.17          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
    1.18           "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
    1.19 -         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
    1.20 +         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
    1.21  
    1.22      val Funs_IntE = (Int_lower2 RS Funs_mono RS
    1.23        (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
    1.24 @@ -124,7 +124,7 @@
    1.25            let
    1.26              val n2 = n div 2;
    1.27              val Type (_, [T1, T2]) = T;
    1.28 -            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    1.29 +            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
    1.30            in
    1.31              if i <= n2 then
    1.32                sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)