src/HOL/Tools/datatype_rep_proofs.ML
changeset 15457 1fbd4aba46e3
parent 15391 797ed46d724b
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jan 24 17:56:18 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Jan 24 17:59:48 2005 +0100
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5      val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
     1.6           In0_eq, In1_eq, In0_not_In1, In1_not_In0,
     1.7 -         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
     1.8 +         Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy o rpair None)
     1.9          ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
    1.10           "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
    1.11           "Lim_inject", "Suml_inject", "Sumr_inject"];
    1.12 @@ -261,9 +261,9 @@
    1.13      (* get axioms from theory *)
    1.14  
    1.15      val newT_iso_axms = map (fn s =>
    1.16 -      (get_thm thy4 ("Abs_" ^ s ^ "_inverse"),
    1.17 -       get_thm thy4 ("Rep_" ^ s ^ "_inverse"),
    1.18 -       get_thm thy4 ("Rep_" ^ s))) new_type_names;
    1.19 +      (get_thm thy4 ("Abs_" ^ s ^ "_inverse", None),
    1.20 +       get_thm thy4 ("Rep_" ^ s ^ "_inverse", None),
    1.21 +       get_thm thy4 ("Rep_" ^ s, None))) new_type_names;
    1.22  
    1.23      (*------------------------------------------------*)
    1.24      (* prove additional theorems:                     *)