src/HOLCF/Tools/pcpodef.ML
changeset 35994 9cc3df9a606e
parent 35912 b0e300bd3a2c
child 36153 1ac501e16a6a
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -193,10 +193,10 @@
     1.4  fun add_podef def opt_name typ set opt_morphs tac thy =
     1.5    let
     1.6      val name = the_default (#1 typ) opt_name;
     1.7 -    val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
     1.8 +    val ((full_tname, info as ({Rep_name, ...}, {type_definition, set_def, ...})), thy2) = thy
     1.9        |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac;
    1.10 -    val oldT = #rep_type info;
    1.11 -    val newT = #abs_type info;
    1.12 +    val oldT = #rep_type (#1 info);
    1.13 +    val newT = #abs_type (#1 info);
    1.14      val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
    1.15  
    1.16      val RepC = Const (Rep_name, newT --> oldT);
    1.17 @@ -235,7 +235,7 @@
    1.18  
    1.19      fun cpodef_result nonempty admissible thy =
    1.20        let
    1.21 -        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
    1.22 +        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
    1.23            |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
    1.24          val (cpo_info, thy3) = thy2
    1.25            |> prove_cpo name newT morphs type_definition set_def below_def admissible;
    1.26 @@ -270,7 +270,7 @@
    1.27      fun pcpodef_result UU_mem admissible thy =
    1.28        let
    1.29          val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
    1.30 -        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
    1.31 +        val ((info as (_, {type_definition, set_def, ...}), below_def), thy2) = thy
    1.32            |> add_podef def (SOME name) typ set opt_morphs tac;
    1.33          val (cpo_info, thy3) = thy2
    1.34            |> prove_cpo name newT morphs type_definition set_def below_def admissible;