merged

--- a/src/HOL/IsaMakefile	Tue Jun 02 08:56:19 2009 +0200
+++ b/src/HOL/IsaMakefile	Tue Jun 02 10:04:03 2009 +0200
@@ -316,6 +316,7 @@
   Library/Abstract_Rat.thy \
   Library/BigO.thy Library/ContNotDenum.thy Library/Efficient_Nat.thy	\
   Library/Euclidean_Space.thy Library/Sum_Of_Squares.thy Library/positivstellensatz.ML	\
+  Library/Convex_Euclidean_Space.thy \
   Library/sum_of_squares.ML Library/Glbs.thy Library/normarith.ML \
   Library/Executable_Set.thy Library/Infinite_Set.thy			\
   Library/FuncSet.thy Library/Permutations.thy Library/Determinants.thy\

--- a/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 08:56:19 2009 +0200
+++ b/src/HOL/Library/Convex_Euclidean_Space.thy	Tue Jun 02 10:04:03 2009 +0200
@@ -1,6 +1,6 @@
-(* Title:      Convex
-   ID:         $Id: 
-   Author:     Robert Himmelmann, TU Muenchen*)
+(*  Title:      HOL/Library/Convex_Euclidean_Space.thy
+    Author:     Robert Himmelmann, TU Muenchen
+*)
 
 header {* Convex sets, functions and related things. *}
 
@@ -2194,7 +2194,7 @@
 lemma convex_interval: "convex {a .. b}" "convex {a<..<b::real^'n::finite}"
   apply(rule_tac[!] is_interval_convex) using is_interval_interval by auto
 
-subsection {* On real^1, is_interval, convex and connected are all equivalent. *}
+subsection {* On @{text "real^1"}, @{text "is_interval"}, @{text "convex"} and @{text "connected"} are all equivalent. *}
 
 lemma is_interval_1:
   "is_interval s \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. dest_vec1 a \<le> dest_vec1 x \<and> dest_vec1 x \<le> dest_vec1 b \<longrightarrow> x \<in> s)"

--- a/src/HOL/Library/Library.thy	Tue Jun 02 08:56:19 2009 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jun 02 10:04:03 2009 +0200
@@ -14,6 +14,7 @@
   Commutative_Ring
   Continuity
   ContNotDenum
+  Convex_Euclidean_Space
   Countable
   Determinants
   Diagonalize

--- a/src/HOL/Tools/datatype_package.ML	Tue Jun 02 08:56:19 2009 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Tue Jun 02 10:04:03 2009 +0200
@@ -386,7 +386,8 @@
     val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       descr sorts thy9;
 
-    val dt_infos = map (make_dt_info NONE (flat descr) sorts induct reccomb_names rec_thms)
+    val dt_infos = map
+      (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms)
       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
         casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
 
@@ -586,7 +587,7 @@
     val _ = (case duplicates (op =) (map fst new_dts) @ duplicates (op =) new_type_names of
       [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
 
-    fun prep_dt_spec (tvs, tname, mx, constrs) (dts', constr_syntax, sorts, i) =
+    fun prep_dt_spec ((tvs, tname, mx, constrs), tname') (dts', constr_syntax, sorts, i) =
       let
         fun prep_constr (cname, cargs, mx') (constrs, constr_syntax', sorts') =
           let
@@ -595,7 +596,7 @@
                 [] => ()
               | vs => error ("Extra type variables on rhs: " ^ commas vs))
           in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
-                Sign.full_name_path tmp_thy (Binding.name_of tname))
+                Sign.full_name_path tmp_thy tname')
                   (Binding.map_name (Syntax.const_name mx') cname),
                    map (dtyp_of_typ new_dts) cargs')],
               constr_syntax' @ [(cname, mx')], sorts'')
@@ -616,7 +617,8 @@
              " in datatype " ^ quote (Binding.str_of tname))
       end;
 
-    val (dts', constr_syntax, sorts', i) = fold prep_dt_spec dts ([], [], [], 0);
+    val (dts', constr_syntax, sorts', i) =
+      fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
     val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
     val dt_info = get_datatypes thy;
     val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;