removed support for set constant definitions in HOLCF {cpo,pcpo,domain}def commands;
removed '(open)', '(set_name)' and '(open set_name)' options

--- a/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -15,7 +15,7 @@
 
 definition "cfun = {f::'a => 'b. cont f}"
 
-cpodef (open) ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
+cpodef ('a, 'b) cfun (infixr "->" 0) = "cfun :: ('a => 'b) set"
   unfolding cfun_def by (auto intro: cont_const adm_cont)
 
 type_notation (xsymbols)

--- a/src/HOL/HOLCF/Fixrec.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Fixrec.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -13,7 +13,7 @@
 
 default_sort cpo
 
-pcpodef (open) 'a match = "UNIV::(one ++ 'a u) set"
+pcpodef 'a match = "UNIV::(one ++ 'a u) set"
 by simp_all
 
 definition

--- a/src/HOL/HOLCF/Lift.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Lift.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -10,7 +10,7 @@
 
 default_sort type
 
-pcpodef (open) 'a lift = "UNIV :: 'a discr u set"
+pcpodef 'a lift = "UNIV :: 'a discr u set"
 by simp_all
 
 lemmas inst_lift_pcpo = Abs_lift_strict [symmetric]

--- a/src/HOL/HOLCF/Sfun.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Sfun.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -8,7 +8,7 @@
 imports Cfun
 begin
 
-pcpodef (open) ('a, 'b) sfun (infixr "->!" 0)
+pcpodef ('a, 'b) sfun (infixr "->!" 0)
   = "{f :: 'a \<rightarrow> 'b. f\<cdot>\<bottom> = \<bottom>}"
 by simp_all
 

--- a/src/HOL/HOLCF/Sprod.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Sprod.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -15,7 +15,7 @@
 
 definition "sprod = {p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
 
-pcpodef (open) ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
+pcpodef ('a, 'b) sprod (infixr "**" 20) = "sprod :: ('a \<times> 'b) set"
   unfolding sprod_def by simp_all
 
 instance sprod :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin

--- a/src/HOL/HOLCF/Ssum.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Ssum.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -19,7 +19,7 @@
       (fst p = TT \<and> fst (snd p) \<noteq> \<bottom> \<and> snd (snd p) = \<bottom>) \<or>
       (fst p = FF \<and> fst (snd p) = \<bottom> \<and> snd (snd p) \<noteq> \<bottom>)}"
 
-pcpodef (open) ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
+pcpodef ('a, 'b) ssum (infixr "++" 10) = "ssum :: (tr \<times> 'a \<times> 'b) set"
   unfolding ssum_def by simp_all
 
 instance ssum :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin

--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Tue Oct 09 17:33:46 2012 +0200
@@ -519,7 +519,7 @@
       let
         val spec = (tbind, map (rpair dummyS) vs, mx)
         val ((_, _, _, {DEFL, ...}), thy) =
-          Domaindef.add_domaindef false NONE spec defl NONE thy
+          Domaindef.add_domaindef spec defl NONE thy
         (* declare domain_defl_simps rules *)
         val thy = Context.theory_map (RepData.add_thm DEFL) thy
       in

--- a/src/HOL/HOLCF/Tools/cpodef.ML	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Oct 09 17:33:46 2012 +0200
@@ -14,27 +14,27 @@
     { Rep_strict: thm, Abs_strict: thm,
       Rep_bottom_iff: thm, Abs_bottom_iff: thm }
 
-  val add_podef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+  val add_podef: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic -> theory ->
     (Typedef.info * thm) * theory
-  val add_cpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+  val add_cpodef: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic * tactic -> theory ->
     (Typedef.info * cpo_info) * theory
-  val add_pcpodef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+  val add_pcpodef: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> tactic * tactic -> theory ->
     (Typedef.info * cpo_info * pcpo_info) * theory
 
-  val cpodef_proof: (bool * binding)
-    * (binding * (string * sort) list * mixfix) * term
+  val cpodef_proof:
+    (binding * (string * sort) list * mixfix) * term
     * (binding * binding) option -> theory -> Proof.state
-  val cpodef_proof_cmd: (bool * binding)
-    * (binding * (string * string option) list * mixfix) * string
+  val cpodef_proof_cmd:
+    (binding * (string * string option) list * mixfix) * string
     * (binding * binding) option -> theory -> Proof.state
-  val pcpodef_proof: (bool * binding)
-    * (binding * (string * sort) list * mixfix) * term
+  val pcpodef_proof:
+    (binding * (string * sort) list * mixfix) * term
     * (binding * binding) option -> theory -> Proof.state
-  val pcpodef_proof_cmd: (bool * binding)
-    * (binding * (string * string option) list * mixfix) * string
+  val pcpodef_proof_cmd:
+    (binding * (string * string option) list * mixfix) * string
     * (binding * binding) option -> theory -> Proof.state
 end
 
@@ -180,11 +180,11 @@
     (newT, oldT, set, morphs)
   end
 
-fun add_podef def opt_name typ set opt_morphs tac thy =
+fun add_podef typ set opt_morphs tac thy =
   let
-    val name = the_default (#1 typ) opt_name
+    val name = #1 typ
     val ((full_tname, info as ({Rep_name, ...}, {type_definition, ...})), thy) = thy
-      |> Typedef.add_typedef_global def opt_name typ set opt_morphs tac
+      |> Typedef.add_typedef_global false NONE typ set opt_morphs tac
     val oldT = #rep_type (#1 info)
     val newT = #abs_type (#1 info)
     val lhs_tfrees = map dest_TFree (snd (dest_Type newT))
@@ -205,14 +205,13 @@
 
 fun prepare_cpodef
       (prep_term: Proof.context -> 'a -> term)
-      (def: bool)
-      (name: binding)
       (typ: binding * (string * sort) list * mixfix)
       (raw_set: 'a)
       (opt_morphs: (binding * binding) option)
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
   let
+    val name = #1 typ
     val (newT, oldT, set, morphs) =
       prepare prep_term name typ raw_set opt_morphs thy
 
@@ -224,7 +223,7 @@
     fun cpodef_result nonempty admissible thy =
       let
         val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
-          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1)
+          |> add_podef typ set opt_morphs (Tactic.rtac nonempty 1)
         val (cpo_info, thy) = thy
           |> prove_cpo name newT morphs type_definition set_def below_def admissible
       in
@@ -234,18 +233,17 @@
     (goal_nonempty, goal_admissible, cpodef_result)
   end
   handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name)
+    cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print (#1 typ))
 
 fun prepare_pcpodef
       (prep_term: Proof.context -> 'a -> term)
-      (def: bool)
-      (name: binding)
       (typ: binding * (string * sort) list * mixfix)
       (raw_set: 'a)
       (opt_morphs: (binding * binding) option)
       (thy: theory)
     : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
   let
+    val name = #1 typ
     val (newT, oldT, set, morphs) =
       prepare prep_term name typ raw_set opt_morphs thy
 
@@ -259,7 +257,7 @@
       let
         val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
         val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
-          |> add_podef def (SOME name) typ set opt_morphs tac
+          |> add_podef typ set opt_morphs tac
         val (cpo_info, thy) = thy
           |> prove_cpo name newT morphs type_definition set_def below_def admissible
         val (pcpo_info, thy) = thy
@@ -271,16 +269,15 @@
     (goal_bottom_mem, goal_admissible, pcpodef_result)
   end
   handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name)
+    cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print (#1 typ))
 
 
 (* tactic interface *)
 
-fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+fun add_cpodef typ set opt_morphs (tac1, tac2) thy =
   let
-    val name = the_default (#1 typ) opt_name
     val (goal1, goal2, cpodef_result) =
-      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy
+      prepare_cpodef Syntax.check_term typ set opt_morphs thy
     val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
       handle ERROR msg => cat_error msg
         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -289,11 +286,10 @@
         ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set))
   in cpodef_result thm1 thm2 thy end
 
-fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+fun add_pcpodef typ set opt_morphs (tac1, tac2) thy =
   let
-    val name = the_default (#1 typ) opt_name
     val (goal1, goal2, pcpodef_result) =
-      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy
+      prepare_pcpodef Syntax.check_term typ set opt_morphs thy
     val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
       handle ERROR msg => cat_error msg
         ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set))
@@ -308,23 +304,23 @@
 local
 
 fun gen_cpodef_proof prep_term prep_constraint
-    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+    ((b, raw_args, mx), set, opt_morphs) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val args = map (apsnd (prep_constraint ctxt)) raw_args
     val (goal1, goal2, make_result) =
-      prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy
+      prepare_cpodef prep_term (b, args, mx) set opt_morphs thy
     fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "cpodef_proof"
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
 
 fun gen_pcpodef_proof prep_term prep_constraint
-    ((def, name), (b, raw_args, mx), set, opt_morphs) thy =
+    ((b, raw_args, mx), set, opt_morphs) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val args = map (apsnd (prep_constraint ctxt)) raw_args
     val (goal1, goal2, make_result) =
-      prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy
+      prepare_pcpodef prep_term (b, args, mx) set opt_morphs thy
     fun after_qed [[th1, th2]] = Proof_Context.background_theory (snd o make_result th1 th2)
       | after_qed _ = raise Fail "pcpodef_proof"
   in Proof.theorem NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end
@@ -344,17 +340,14 @@
 (** outer syntax **)
 
 val typedef_proof_decl =
-  Scan.optional (@{keyword "("} |--
-      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
-        Parse.binding >> (fn s => (true, SOME s)))
-        --| @{keyword ")"}) (true, NONE) --
-    (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
-    (@{keyword "="} |-- Parse.term) --
-    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+  (Parse.type_args_constrained -- Parse.binding) -- Parse.opt_mixfix --
+  (@{keyword "="} |-- Parse.term) --
+  Scan.option
+    (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
 
-fun mk_pcpodef_proof pcpo ((((((def, opt_name), (args, t)), mx), A), morphs)) =
+fun mk_pcpodef_proof pcpo ((((args, t), mx), A), morphs) =
   (if pcpo then pcpodef_proof_cmd else cpodef_proof_cmd)
-    ((def, the_default t opt_name), (t, args, mx), A, morphs)
+    ((t, args, mx), A, morphs)
 
 val _ =
   Outer_Syntax.command @{command_spec "pcpodef"}

--- a/src/HOL/HOLCF/Tools/domaindef.ML	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML	Tue Oct 09 17:33:46 2012 +0200
@@ -17,11 +17,11 @@
       DEFL : thm
     }
 
-  val add_domaindef: bool -> binding option -> binding * (string * sort) list * mixfix ->
+  val add_domaindef: binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> theory ->
     (Typedef.info * Cpodef.cpo_info * Cpodef.pcpo_info * rep_info) * theory
 
-  val domaindef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string
+  val domaindef_cmd: (binding * (string * string option) list * mixfix) * string
     * (binding * binding) option -> theory -> theory
 end
 
@@ -78,8 +78,6 @@
 
 fun gen_add_domaindef
       (prep_term: Proof.context -> 'a -> term)
-      (def: bool)
-      (name: binding)
       (typ as (tname, raw_args, _) : binding * (string * sort) list * mixfix)
       (raw_defl: 'a)
       (opt_morphs: (binding * binding) option)
@@ -106,7 +104,7 @@
 
     (*morphisms*)
     val morphs = opt_morphs
-      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
+      |> the_default (Binding.prefix_name "Rep_" tname, Binding.prefix_name "Abs_" tname)
 
     (*set*)
     val set = @{term "defl_set :: udom defl => udom set"} $ defl
@@ -115,7 +113,7 @@
     val tac1 = rtac @{thm defl_set_bottom} 1
     val tac2 = rtac @{thm adm_defl_set} 1
     val ((info, cpo_info, pcpo_info), thy) = thy
-      |> Cpodef.add_pcpodef def (SOME name) typ set (SOME morphs) (tac1, tac2)
+      |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2)
 
     (*definitions*)
     val Rep_const = Const (#Rep_name (#1 info), newT --> udomT)
@@ -134,7 +132,7 @@
         Abs ("t", Term.itselfT newT,
           mk_capply (@{const liftdefl_of}, defl_const newT $ Logic.mk_type newT)))
 
-    val name_def = Thm.def_binding name
+    val name_def = Thm.def_binding tname
     val emb_bind = (Binding.prefix_name "emb_" name_def, [])
     val prj_bind = (Binding.prefix_name "prj_" name_def, [])
     val defl_bind = (Binding.prefix_name "defl_" name_def, [])
@@ -179,9 +177,9 @@
     (*other theorems*)
     val defl_thm' = Thm.transfer thy defl_def
     val (DEFL_thm, thy) = thy
-      |> Sign.add_path (Binding.name_of name)
+      |> Sign.add_path (Binding.name_of tname)
       |> Global_Theory.add_thm
-         ((Binding.prefix_name "DEFL_" name,
+         ((Binding.prefix_name "DEFL_" tname,
           Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
       ||> Sign.restore_naming thy
 
@@ -193,35 +191,28 @@
     ((info, cpo_info, pcpo_info, rep_info), thy)
   end
   handle ERROR msg =>
-    cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print name)
+    cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print tname)
 
-fun add_domaindef def opt_name typ defl opt_morphs thy =
-  let
-    val name = the_default (#1 typ) opt_name
-  in
-    gen_add_domaindef Syntax.check_term def name typ defl opt_morphs thy
-  end
+fun add_domaindef typ defl opt_morphs thy =
+  gen_add_domaindef Syntax.check_term typ defl opt_morphs thy
 
-fun domaindef_cmd ((def, name), (b, raw_args, mx), A, morphs) thy =
+fun domaindef_cmd ((b, raw_args, mx), A, morphs) thy =
   let
     val ctxt = Proof_Context.init_global thy
     val args = map (apsnd (Typedecl.read_constraint ctxt)) raw_args
-  in snd (gen_add_domaindef Syntax.read_term def name (b, args, mx) A morphs thy) end
+  in snd (gen_add_domaindef Syntax.read_term (b, args, mx) A morphs thy) end
 
 
 (** outer syntax **)
 
 val domaindef_decl =
-  Scan.optional (@{keyword "("} |--
-      ((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
-        Parse.binding >> (fn s => (true, SOME s)))
-        --| @{keyword ")"}) (true, NONE) --
-    (Parse.type_args_constrained -- Parse.binding) --
-    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
-    Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
+  (Parse.type_args_constrained -- Parse.binding) --
+  Parse.opt_mixfix -- (@{keyword "="} |-- Parse.term) --
+  Scan.option
+    (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
 
-fun mk_domaindef ((((((def, opt_name), (args, t)), mx), A), morphs)) =
-  domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
+fun mk_domaindef (((((args, t)), mx), A), morphs) =
+  domaindef_cmd ((t, args, mx), A, morphs)
 
 val _ =
   Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"

--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 16:58:36 2012 +0200
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Tue Oct 09 17:33:46 2012 +0200
@@ -80,13 +80,13 @@
 
 text {* Use @{text pcpodef} with the appropriate type combinator. *}
 
-pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
+pcpodef 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
-pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
+pcpodef 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
-pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
+pcpodef 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"
 by (rule defl_set_bottom, rule adm_defl_set)
 
 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}