# HG changeset patch
# User wenzelm
# Date 1272468598 -7200
# Node ID 620f899158d421e25a3016ed75b281732902b85b
# Parent  7ec5ceef117b151348f173b68431f90ebb317e06# Parent  c051d18994890c354d8d38043e7d04cd596f4c7a
merged

diff -r 7ec5ceef117b -r 620f899158d4 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 16:56:03 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed Apr 28 17:29:58 2010 +0200
@@ -10,7 +10,7 @@
 
 default_sort type
 
-types 'a Seq = "'a::type lift seq"
+types 'a Seq = "'a lift seq"
 
 consts
 
diff -r 7ec5ceef117b -r 620f899158d4 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Pure/Isar/typedecl.ML	Wed Apr 28 17:29:58 2010 +0200
@@ -82,10 +82,12 @@
 
 (* type abbreviations *)
 
+local
+
 fun gen_abbrev prep_typ (b, vs, mx) raw_rhs lthy =
   let
     val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
-    val rhs = prep_typ lthy raw_rhs
+    val rhs = prep_typ b lthy raw_rhs
       handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   in
     lthy
@@ -94,8 +96,23 @@
     |> pair name
   end;
 
-val abbrev = gen_abbrev ProofContext.cert_typ_syntax;
-val abbrev_cmd = gen_abbrev ProofContext.read_typ_syntax;
+fun read_abbrev b ctxt raw_rhs =
+  let
+    val rhs = ProofContext.read_typ_syntax (ctxt |> ProofContext.set_defsort []) raw_rhs;
+    val ignored = Term.fold_atyps_sorts (fn (_, []) => I | (T, _) => insert (op =) T) rhs [];
+    val _ =
+      if null ignored then ()
+      else warning ("Ignoring sort constraints in type variables(s): " ^
+        commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
+        "\nin type abbreviation " ^ quote (Binding.str_of b));
+  in rhs end;
+
+in
+
+val abbrev = gen_abbrev (K ProofContext.cert_typ_syntax);
+val abbrev_cmd = gen_abbrev read_abbrev;
+
+end;
 
 fun abbrev_global decl rhs =
   Theory_Target.init NONE
diff -r 7ec5ceef117b -r 620f899158d4 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Pure/axclass.ML	Wed Apr 28 17:29:58 2010 +0200
@@ -190,9 +190,9 @@
 
 infix 0 RSO;
 
-fun (SOME a RSO SOME b) = SOME (a RS b)
-  | (x RSO NONE) = x
-  | (NONE RSO y) = y;
+fun (SOME a) RSO (SOME b) = SOME (a RS b)
+  | x RSO NONE = x
+  | NONE RSO y = y;
 
 fun the_classrel thy (c1, c2) =
   (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
diff -r 7ec5ceef117b -r 620f899158d4 src/Tools/jEdit/README_BUILD
--- a/src/Tools/jEdit/README_BUILD	Wed Apr 28 16:56:03 2010 +0200
+++ b/src/Tools/jEdit/README_BUILD	Wed Apr 28 17:29:58 2010 +0200
@@ -74,3 +74,17 @@
 releases. (See
 http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html)
 -----------------------------------------------------------------------
+
+
+Known problems with Mac OS
+==========================
+
+- The MacOSX plugin disrupts regular C-X/C/V operations, e.g. between
+  the editor and the Console plugin, which is a standard swing text
+  box.  Similar for search boxes etc.
+
+- Anti-aliasing does not really work as well as for Linux or Windows.
+  (General Apple/Swing problem?)
+
+- Font.createFont mangles the font family of non-regular fonts,
+  e.g. bold.