removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
authorhuffman
Tue Oct 09 17:33:46 2012 +0200 (2012-10-09)
changeset 49759ecf1d5d87e5e
parent 49758 718f10c8bbfc
child 49760 0721b1311327
child 49770 cf6a78acf445
removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
removed '(open)', '(set_name)' and '(open set_name)' options
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/Lift.thy
src/HOL/HOLCF/Sfun.thy
src/HOL/HOLCF/Sprod.thy
src/HOL/HOLCF/Ssum.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/HOLCF/ex/Domain_Proofs.thy
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 16:58:36 2012 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 17:33:46 2012 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  
     1.5  definition "cfun = {f::'a => 'b. cont f}"
     1.6  
     1.7 -cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
     1.8 +cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
     1.9    unfolding cfun_def by (auto intro: cont_const adm_cont)
    1.10  
    1.11  type_notation (xsymbols)
     2.1 --- a/src/HOL/HOLCF/Fixrec.thy	Tue Oct 09 16:58:36 2012 +0200
     2.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Oct 09 17:33:46 2012 +0200
     2.3 @@ -13,7 +13,7 @@
     2.4  
     2.5  default_sort cpo
     2.6  
     2.7 -pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set"
     2.8 +pcpodef 'a match = "UNIV::(one ++ 'a u) set"
     2.9  by simp_all
    2.10  
    2.11  definition
     3.1 --- a/src/HOL/HOLCF/Lift.thy	Tue Oct 09 16:58:36 2012 +0200
     3.2 +++ b/src/HOL/HOLCF/Lift.thy	Tue Oct 09 17:33:46 2012 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  default_sort type
     3.6  
     3.7 -pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
     3.8 +pcpodef 'a lift = "UNIV :: 'a discr u set"
     3.9  by simp_all
    3.10  
    3.11  lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]
     4.1 --- a/src/HOL/HOLCF/Sfun.thy	Tue Oct 09 16:58:36 2012 +0200
     4.2 +++ b/src/HOL/HOLCF/Sfun.thy	Tue Oct 09 17:33:46 2012 +0200
     4.3 @@ -8,7 +8,7 @@
     4.4  imports Cfun
     4.5  begin
     4.6  
     4.7 -pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
     4.8 +pcpodef ('a, 'b) sfun (infixr "->!" 0)
     4.9    = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
    4.10  by simp_all
    4.11  
     5.1 --- a/src/HOL/HOLCF/Sprod.thy	Tue Oct 09 16:58:36 2012 +0200
     5.2 +++ b/src/HOL/HOLCF/Sprod.thy	Tue Oct 09 17:33:46 2012 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  
     5.5  definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
     5.6  
     5.7 -pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
     5.8 +pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
     5.9    unfolding sprod_def by simp_all
    5.10  
    5.11  instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
     6.1 --- a/src/HOL/HOLCF/Ssum.thy	Tue Oct 09 16:58:36 2012 +0200
     6.2 +++ b/src/HOL/HOLCF/Ssum.thy	Tue Oct 09 17:33:46 2012 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4        (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
     6.5        (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
     6.6  
     6.7 -pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
     6.8 +pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
     6.9    unfolding ssum_def by simp_all
    6.10  
    6.11  instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
     7.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 09 16:58:36 2012 +0200
     7.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 09 17:33:46 2012 +0200
     7.3 @@ -519,7 +519,7 @@
     7.4        let
     7.5          val spec = (tbind, map (rpair dummyS) vs, mx)
     7.6          val ((_, _, _, {DEFL, ...}), thy) =
     7.7 -          Domaindef.add_domaindef false NONE spec defl NONE thy
     7.8 +          Domaindef.add_domaindef spec defl NONE thy
     7.9          (* declare domain_defl_simps rules *)
    7.10          val thy = Context.theory_map (RepData.add_thm DEFL) thy
    7.11        in
     8.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Tue Oct 09 16:58:36 2012 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Oct 09 17:33:46 2012 +0200
     8.3 @@ -14,27 +14,27 @@
     8.4      { Rep_strict: thm, Abs_strict: thm,
     8.5        Rep_bottom_iff: thm, Abs_bottom_iff: thm }
     8.6  
     8.7 -  val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     8.8 +  val add_podef: binding * (string * sort) list * mixfix ->
     8.9      term -> (binding * binding) option -> tactic -> theory ->
    8.10      (Typedef.info * thm) * theory
    8.11 -  val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    8.12 +  val add_cpodef: binding * (string * sort) list * mixfix ->
    8.13      term -> (binding * binding) option -> tactic * tactic -> theory ->
    8.14      (Typedef.info * cpo_info) * theory
    8.15 -  val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
    8.16 +  val add_pcpodef: binding * (string * sort) list * mixfix ->
    8.17      term -> (binding * binding) option -> tactic * tactic -> theory ->
    8.18      (Typedef.info * cpo_info * pcpo_info) * theory
    8.19  
    8.20 -  val cpodef_proof: (bool * binding)
    8.21 -    * (binding * (string * sort) list * mixfix) * term
    8.22 +  val cpodef_proof:
    8.23 +    (binding * (string * sort) list * mixfix) * term
    8.24      * (binding * binding) option -> theory -> Proof.state
    8.25 -  val cpodef_proof_cmd: (bool * binding)
    8.26 -    * (binding * (string * string option) list * mixfix) * string
    8.27 +  val cpodef_proof_cmd:
    8.28 +    (binding * (string * string option) list * mixfix) * string
    8.29      * (binding * binding) option -> theory -> Proof.state
    8.30 -  val pcpodef_proof: (bool * binding)
    8.31 -    * (binding * (string * sort) list * mixfix) * term
    8.32 +  val pcpodef_proof:
    8.33 +    (binding * (string * sort) list * mixfix) * term
    8.34      * (binding * binding) option -> theory -> Proof.state
    8.35 -  val pcpodef_proof_cmd: (bool * binding)
    8.36 -    * (binding * (string * string option) list * mixfix) * string
    8.37 +  val pcpodef_proof_cmd:
    8.38 +    (binding * (string * string option) list * mixfix) * string
    8.39      * (binding * binding) option -> theory -> Proof.state
    8.40  end
    8.41  
    8.42 @@ -180,11 +180,11 @@
    8.43      (newT, oldT, set, morphs)
    8.44    end
    8.45  
    8.46 -fun add_podef def opt_name typ set opt_morphs tac thy =
    8.47 +fun add_podef typ set opt_morphs tac thy =
    8.48    let
    8.49 -    val name = the_default (#1 typ) opt_name
    8.50 +    val name = #1 typ
    8.51      val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
    8.52 -      |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
    8.53 +      |> Typedef.add_typedef_global false NONE typ set opt_morphs tac
    8.54      val oldT = #rep_type (#1 info)
    8.55      val newT = #abs_type (#1 info)
    8.56      val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
    8.57 @@ -205,14 +205,13 @@
    8.58  
    8.59  fun prepare_cpodef
    8.60        (prep_term: Proof.context -> 'a -> term)
    8.61 -      (def: bool)
    8.62 -      (name: binding)
    8.63        (typ: binding * (string * sort) list * mixfix)
    8.64        (raw_set: 'a)
    8.65        (opt_morphs: (binding * binding) option)
    8.66        (thy: theory)
    8.67      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
    8.68    let
    8.69 +    val name = #1 typ
    8.70      val (newT, oldT, set, morphs) =
    8.71        prepare prep_term name typ raw_set opt_morphs thy
    8.72  
    8.73 @@ -224,7 +223,7 @@
    8.74      fun cpodef_result nonempty admissible thy =
    8.75        let
    8.76          val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
    8.77 -          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1)
    8.78 +          |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
    8.79          val (cpo_info, thy) = thy
    8.80            |> prove_cpo name newT morphs type_definition set_def below_def admissible
    8.81        in
    8.82 @@ -234,18 +233,17 @@
    8.83      (goal_nonempty, goal_admissible, cpodef_result)
    8.84    end
    8.85    handle ERROR msg =>
    8.86 -    cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name)
    8.87 +    cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print (#1 typ))
    8.88  
    8.89  fun prepare_pcpodef
    8.90        (prep_term: Proof.context -> 'a -> term)
    8.91 -      (def: bool)
    8.92 -      (name: binding)
    8.93        (typ: binding * (string * sort) list * mixfix)
    8.94        (raw_set: 'a)
    8.95        (opt_morphs: (binding * binding) option)
    8.96        (thy: theory)
    8.97      : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
    8.98    let
    8.99 +    val name = #1 typ
   8.100      val (newT, oldT, set, morphs) =
   8.101        prepare prep_term name typ raw_set opt_morphs thy
   8.102  
   8.103 @@ -259,7 +257,7 @@
   8.104        let
   8.105          val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
   8.106          val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
   8.107 -          |> add_podef def (SOME name) typ set opt_morphs tac
   8.108 +          |> add_podef typ set opt_morphs tac
   8.109          val (cpo_info, thy) = thy
   8.110            |> prove_cpo name newT morphs type_definition set_def below_def admissible
   8.111          val (pcpo_info, thy) = thy
   8.112 @@ -271,16 +269,15 @@
   8.113      (goal_bottom_mem, goal_admissible, pcpodef_result)
   8.114    end
   8.115    handle ERROR msg =>
   8.116 -    cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name)
   8.117 +    cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ))
   8.118  
   8.119  
   8.120  (* tactic interface *)
   8.121  
   8.122 -fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
   8.123 +fun add_cpodef typ set opt_morphs (tac1, tac2) thy =
   8.124    let
   8.125 -    val name = the_default (#1 typ) opt_name
   8.126      val (goal1, goal2, cpodef_result) =
   8.127 -      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy
   8.128 +      prepare_cpodef Syntax.check_term typ set opt_morphs thy
   8.129      val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
   8.130        handle ERROR msg => cat_error msg
   8.131          ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
   8.132 @@ -289,11 +286,10 @@
   8.133          ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
   8.134    in cpodef_result thm1 thm2 thy end
   8.135  
   8.136 -fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
   8.137 +fun add_pcpodef typ set opt_morphs (tac1, tac2) thy =
   8.138    let
   8.139 -    val name = the_default (#1 typ) opt_name
   8.140      val (goal1, goal2, pcpodef_result) =
   8.141 -      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy
   8.142 +      prepare_pcpodef Syntax.check_term typ set opt_morphs thy
   8.143      val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
   8.144        handle ERROR msg => cat_error msg
   8.145          ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
   8.146 @@ -308,23 +304,23 @@
   8.147  local
   8.148  
   8.149  fun gen_cpodef_proof prep_term prep_constraint
   8.150 -    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   8.151 +    ((b, raw_args, mx), set, opt_morphs) thy =
   8.152    let
   8.153      val ctxt = Proof_Context.init_global thy
   8.154      val args = map (apsnd (prep_constraint ctxt)) raw_args
   8.155      val (goal1, goal2, make_result) =
   8.156 -      prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy
   8.157 +      prepare_cpodef prep_term (b, args, mx) set opt_morphs thy
   8.158      fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
   8.159        | after_qed _ = raise Fail "cpodef_proof"
   8.160    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
   8.161  
   8.162  fun gen_pcpodef_proof prep_term prep_constraint
   8.163 -    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
   8.164 +    ((b, raw_args, mx), set, opt_morphs) thy =
   8.165    let
   8.166      val ctxt = Proof_Context.init_global thy
   8.167      val args = map (apsnd (prep_constraint ctxt)) raw_args
   8.168      val (goal1, goal2, make_result) =
   8.169 -      prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy
   8.170 +      prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy
   8.171      fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
   8.172        | after_qed _ = raise Fail "pcpodef_proof"
   8.173    in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
   8.174 @@ -344,17 +340,14 @@
   8.175  (** outer syntax **)
   8.176  
   8.177  val typedef_proof_decl =
   8.178 -  Scan.optional (@{keyword "("} |--
   8.179 -      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
   8.180 -        Parse.binding >> (fn s => (true, SOME s)))
   8.181 -        --| @{keyword ")"}) (true, NONE) --
   8.182 -    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
   8.183 -    (@{keyword "="} |-- Parse.term) --
   8.184 -    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   8.185 +  (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
   8.186 +  (@{keyword "="} |-- Parse.term) --
   8.187 +  Scan.option
   8.188 +    (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   8.189  
   8.190 -fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   8.191 +fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) =
   8.192    (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
   8.193 -    ((def, the_default t opt_name), (t, args, mx), A, morphs)
   8.194 +    ((t, args, mx), A, morphs)
   8.195  
   8.196  val _ =
   8.197    Outer_Syntax.command @{command_spec "pcpodef"}
     9.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Oct 09 16:58:36 2012 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Oct 09 17:33:46 2012 +0200
     9.3 @@ -17,11 +17,11 @@
     9.4        DEFL : thm
     9.5      }
     9.6  
     9.7 -  val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     9.8 +  val add_domaindef: binding * (string * sort) list * mixfix ->
     9.9      term -> (binding * binding) option -> theory ->
    9.10      (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
    9.11  
    9.12 -  val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
    9.13 +  val domaindef_cmd: (binding * (string * string option) list * mixfix) * string
    9.14      * (binding * binding) option -> theory -> theory
    9.15  end
    9.16  
    9.17 @@ -78,8 +78,6 @@
    9.18  
    9.19  fun gen_add_domaindef
    9.20        (prep_term: Proof.context -> 'a -> term)
    9.21 -      (def: bool)
    9.22 -      (name: binding)
    9.23        (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
    9.24        (raw_defl: 'a)
    9.25        (opt_morphs: (binding * binding) option)
    9.26 @@ -106,7 +104,7 @@
    9.27  
    9.28      (*morphisms*)
    9.29      val morphs = opt_morphs
    9.30 -      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
    9.31 +      |> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname)
    9.32  
    9.33      (*set*)
    9.34      val set = @{term "defl_set :: udom defl => udom set"} $ defl
    9.35 @@ -115,7 +113,7 @@
    9.36      val tac1 = rtac @{thm defl_set_bottom} 1
    9.37      val tac2 = rtac @{thm adm_defl_set} 1
    9.38      val ((info, cpo_info, pcpo_info), thy) = thy
    9.39 -      |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2)
    9.40 +      |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
    9.41  
    9.42      (*definitions*)
    9.43      val Rep_const = Const (#Rep_name (#1 info), newT --> udomT)
    9.44 @@ -134,7 +132,7 @@
    9.45          Abs ("t", Term.itselfT newT,
    9.46            mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
    9.47  
    9.48 -    val name_def = Thm.def_binding name
    9.49 +    val name_def = Thm.def_binding tname
    9.50      val emb_bind = (Binding.prefix_name "emb_" name_def, [])
    9.51      val prj_bind = (Binding.prefix_name "prj_" name_def, [])
    9.52      val defl_bind = (Binding.prefix_name "defl_" name_def, [])
    9.53 @@ -179,9 +177,9 @@
    9.54      (*other theorems*)
    9.55      val defl_thm' = Thm.transfer thy defl_def
    9.56      val (DEFL_thm, thy) = thy
    9.57 -      |> Sign.add_path (Binding.name_of name)
    9.58 +      |> Sign.add_path (Binding.name_of tname)
    9.59        |> Global_Theory.add_thm
    9.60 -         ((Binding.prefix_name "DEFL_" name,
    9.61 +         ((Binding.prefix_name "DEFL_" tname,
    9.62            Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
    9.63        ||> Sign.restore_naming thy
    9.64  
    9.65 @@ -193,35 +191,28 @@
    9.66      ((info, cpo_info, pcpo_info, rep_info), thy)
    9.67    end
    9.68    handle ERROR msg =>
    9.69 -    cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print name)
    9.70 +    cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname)
    9.71  
    9.72 -fun add_domaindef def opt_name typ defl opt_morphs thy =
    9.73 -  let
    9.74 -    val name = the_default (#1 typ) opt_name
    9.75 -  in
    9.76 -    gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy
    9.77 -  end
    9.78 +fun add_domaindef typ defl opt_morphs thy =
    9.79 +  gen_add_domaindef Syntax.check_term typ defl opt_morphs thy
    9.80  
    9.81 -fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
    9.82 +fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy =
    9.83    let
    9.84      val ctxt = Proof_Context.init_global thy
    9.85      val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args
    9.86 -  in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end
    9.87 +  in snd (gen_add_domaindef Syntax.read_term (b, args, mx) A morphs thy) end
    9.88  
    9.89  
    9.90  (** outer syntax **)
    9.91  
    9.92  val domaindef_decl =
    9.93 -  Scan.optional (@{keyword "("} |--
    9.94 -      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
    9.95 -        Parse.binding >> (fn s => (true, SOME s)))
    9.96 -        --| @{keyword ")"}) (true, NONE) --
    9.97 -    (Parse.type_args_constrained -- Parse.binding) --
    9.98 -    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
    9.99 -    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   9.100 +  (Parse.type_args_constrained -- Parse.binding) --
   9.101 +  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
   9.102 +  Scan.option
   9.103 +    (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
   9.104  
   9.105 -fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
   9.106 -  domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
   9.107 +fun mk_domaindef (((((args, t)), mx), A), morphs) =
   9.108 +  domaindef_cmd ((t, args, mx), A, morphs)
   9.109  
   9.110  val _ =
   9.111    Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
    10.1 --- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 16:58:36 2012 +0200
    10.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 17:33:46 2012 +0200
    10.3 @@ -80,13 +80,13 @@
    10.4  
    10.5  text {* Use @{text pcpodef} with the appropriate type combinator. *}
    10.6  
    10.7 -pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
    10.8 +pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
    10.9  by (rule defl_set_bottom, rule adm_defl_set)
   10.10  
   10.11 -pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
   10.12 +pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
   10.13  by (rule defl_set_bottom, rule adm_defl_set)
   10.14  
   10.15 -pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
   10.16 +pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
   10.17  by (rule defl_set_bottom, rule adm_defl_set)
   10.18  
   10.19  text {* Prove rep instance using lemma @{text typedef_rep_class}. *}