src/HOLCF/Tools/repdef.ML
changeset 35994 9cc3df9a606e
parent 35904 0c13e28e5e41
child 36153 1ac501e16a6a
     1.1 --- a/src/HOLCF/Tools/repdef.ML	Sat Mar 27 18:43:11 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/repdef.ML	Sat Mar 27 21:38:38 2010 +0100
     1.3 @@ -95,8 +95,8 @@
     1.4        |> Pcpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2);
     1.5  
     1.6      (*definitions*)
     1.7 -    val Rep_const = Const (#Rep_name info, newT --> udomT);
     1.8 -    val Abs_const = Const (#Abs_name info, udomT --> newT);
     1.9 +    val Rep_const = Const (#Rep_name (#1 info), newT --> udomT);
    1.10 +    val Abs_const = Const (#Abs_name (#1 info), udomT --> newT);
    1.11      val emb_eqn = Logic.mk_equals (emb_const newT, cabs_const (newT, udomT) $ Rep_const);
    1.12      val prj_eqn = Logic.mk_equals (prj_const newT, cabs_const (udomT, newT) $
    1.13        Abs ("x", udomT, Abs_const $ mk_cast (defl, Bound 0)));
    1.14 @@ -125,8 +125,8 @@
    1.15      val approx_def = singleton (ProofContext.export lthy ctxt_thy) approx_ldef;
    1.16      val type_definition_thm =
    1.17        MetaSimplifier.rewrite_rule
    1.18 -        (the_list (#set_def info))
    1.19 -        (#type_definition info);
    1.20 +        (the_list (#set_def (#2 info)))
    1.21 +        (#type_definition (#2 info));
    1.22      val typedef_thms =
    1.23        [type_definition_thm, #below_def cpo_info, emb_def, prj_def, approx_def];
    1.24      val thy = lthy