src/HOL/Tools/datatype_rep_proofs.ML
changeset 7293 959e060f4a2f
parent 7257 745cfc8871e2
child 7499 23e090051cb8
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 18:36:41 1999 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Aug 19 19:00:42 1999 +0200
@@ -47,16 +47,16 @@
     val Datatype_thy = theory "Datatype";
     val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
     val [In0_name, In1_name, Scons_name, Leaf_name, Numb_name, Lim_name,
-      Funs_name, o_name] =
+      Funs_name, o_name, sum_case_name] =
       map (Sign.intern_const (Theory.sign_of Datatype_thy))
-        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o"];
+        ["In0", "In1", "Scons", "Leaf", "Numb", "Lim", "Funs", "op o", "sum_case"];
 
     val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
          In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
-         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty] = map (get_thm Datatype_thy)
+         Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
         ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
          "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
-         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty"];
+         "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
 
     val Funs_IntE = (Int_lower2 RS Funs_mono RS
       (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
@@ -124,7 +124,7 @@
           let
             val n2 = n div 2;
             val Type (_, [T1, T2]) = T;
-            val sum_case = Const ("basic_sum_case", [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+            val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
           in
             if i <= n2 then
               sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)