src/HOLCF/Tools/pcpodef.ML
changeset 35129 ed24ba6f69aa
parent 35021 c839a4c670c6
child 35203 ef65a2218c31
     1.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon Feb 15 15:50:41 2010 +0100
     1.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon Feb 15 17:17:51 2010 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4  fun declare_type_name a =
     1.5    Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
     1.6  
     1.7 -fun prepare prep_term name (t, vs, mx) raw_set opt_morphs thy =
     1.8 +fun prepare prep_term name (tname, vs, mx) raw_set opt_morphs thy =
     1.9    let
    1.10      val _ = Theory.requires thy "Pcpodef" "pcpodefs";
    1.11      val ctxt = ProofContext.init thy;
    1.12 @@ -168,7 +168,6 @@
    1.13      (*lhs*)
    1.14      val defS = Sign.defaultS thy;
    1.15      val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
    1.16 -    val tname = Binding.map_name (Syntax.type_name mx) t;
    1.17      val full_tname = Sign.full_name thy tname;
    1.18      val newT = Type (full_tname, map TFree lhs_tfrees);
    1.19  
    1.20 @@ -346,7 +345,7 @@
    1.21  
    1.22  fun mk_pcpodef_proof pcpo ((((((def, opt_name), (vs, t)), mx), A), morphs)) =
    1.23    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
    1.24 -    ((def, the_default (Binding.map_name (Syntax.type_name mx) t) opt_name), (t, vs, mx), A, morphs);
    1.25 +    ((def, the_default t opt_name), (t, vs, mx), A, morphs);
    1.26  
    1.27  val _ =
    1.28    OuterSyntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)" K.thy_goal