merged

--- a/src/HOL/Lattices.thy	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/HOL/Lattices.thy	Thu Sep 03 20:26:07 2009 +0200
@@ -413,12 +413,11 @@
 subsection {* @{const min}/@{const max} on linear orders as
   special case of @{const inf}/@{const sup} *}
 
-sublocale linorder < min_max!: distrib_lattice less_eq less "Orderings.ord.min less_eq" "Orderings.ord.max less_eq"
+sublocale linorder < min_max!: distrib_lattice less_eq less min max
 proof
   fix x y z
-  show "Orderings.ord.max less_eq x (Orderings.ord.min less_eq y z) =
-    Orderings.ord.min less_eq (Orderings.ord.max less_eq x y) (Orderings.ord.max less_eq x z)"
-  unfolding min_def max_def by auto
+  show "max x (min y z) = min (max x y) (max x z)"
+    by (auto simp add: min_def max_def)
 qed (auto simp add: min_def max_def not_le less_imp_le)
 
 lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
@@ -514,9 +513,6 @@
   inf_compl_bot sup_compl_top diff_eq)
 
 
-text {* redundant bindings *}
-
-
 no_notation
   less_eq  (infix "\<sqsubseteq>" 50) and
   less (infix "\<sqsubset>" 50) and

--- a/src/Pure/Isar/expression.ML	Thu Sep 03 18:41:58 2009 +0200
+++ b/src/Pure/Isar/expression.ML	Thu Sep 03 20:26:07 2009 +0200
@@ -839,7 +839,7 @@
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = Locale.init target thy;
+    val target_ctxt = TheoryTarget.init (SOME target) thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency