merged

--- a/src/HOL/Set.thy	Fri Mar 09 20:04:19 2012 +0100
+++ b/src/HOL/Set.thy	Fri Mar 09 22:05:15 2012 +0100
@@ -97,28 +97,28 @@
 begin
 
 definition less_eq_set where
-  "less_eq_set A B = less_eq (\<lambda>x. member x A) (\<lambda>x. member x B)"
+  "A \<le> B \<longleftrightarrow> (\<lambda>x. member x A) \<le> (\<lambda>x. member x B)"
 
 definition less_set where
-  "less_set A B = less (\<lambda>x. member x A) (\<lambda>x. member x B)"
+  "A < B \<longleftrightarrow> (\<lambda>x. member x A) < (\<lambda>x. member x B)"
 
 definition inf_set where
-  "inf_set A B = Collect (inf (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A \<sqinter> B = Collect ((\<lambda>x. member x A) \<sqinter> (\<lambda>x. member x B))"
 
 definition sup_set where
-  "sup_set A B = Collect (sup (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A \<squnion> B = Collect ((\<lambda>x. member x A) \<squnion> (\<lambda>x. member x B))"
 
 definition bot_set where
-  "bot = Collect bot"
+  "\<bottom> = Collect \<bottom>"
 
 definition top_set where
-  "top = Collect top"
+  "\<top> = Collect \<top>"
 
 definition uminus_set where
-  "uminus A = Collect (uminus (\<lambda>x. member x A))"
+  "- A = Collect (- (\<lambda>x. member x A))"
 
 definition minus_set where
-  "minus_set A B = Collect (minus (\<lambda>x. member x A) (\<lambda>x. member x B))"
+  "A - B = Collect ((\<lambda>x. member x A) - (\<lambda>x. member x B))"
 
 instance proof
 qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
@@ -1907,3 +1907,4 @@
 *}
 
 end
+

--- a/src/HOL/Tools/enriched_type.ML	Fri Mar 09 20:04:19 2012 +0100
+++ b/src/HOL/Tools/enriched_type.ML	Fri Mar 09 22:05:15 2012 +0100
@@ -170,6 +170,33 @@
         val (Ts'', T'') = split_last Ts';
       in (Ts'', T'', T') end;
 
+fun analyze_mapper ctxt input_mapper =
+  let
+    val T = fastype_of input_mapper;
+    val _ = Type.no_tvars T;
+    val _ =
+      if null (subtract (op =) (Term.add_tfreesT T []) (Term.add_tfrees input_mapper []))
+      then ()
+      else error ("Illegal additional type variable(s) in term: " ^ Syntax.string_of_term ctxt input_mapper);
+    val _ =
+      if null (Term.add_vars (singleton
+        (Variable.export_terms (Variable.auto_fixes input_mapper ctxt) ctxt) input_mapper) [])
+      then ()
+      else error ("Illegal locally free variable(s) in term: "
+        ^ Syntax.string_of_term ctxt input_mapper);;
+    val mapper = singleton (Variable.polymorphic ctxt) input_mapper;
+    val _ =
+      if null (Term.add_tfreesT (fastype_of mapper) []) then ()
+      else error ("Illegal locally fixed type variable(s) in type: " ^ Syntax.string_of_typ ctxt T);
+    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
+      | add_tycos _ = I;
+    val tycos = add_tycos T [];
+    val tyco = if tycos = ["fun"] then "fun"
+      else case remove (op =) "fun" tycos
+       of [tyco] => tyco
+        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ ctxt T);
+  in (mapper, T, tyco) end;
+
 fun analyze_variances ctxt tyco T =
   let
     fun bad_typ () = error ("Bad mapper type: " ^ Syntax.string_of_typ ctxt T);
@@ -198,19 +225,7 @@
 
 fun gen_enriched_type prep_term some_prfx raw_mapper lthy =
   let
-    val input_mapper = prep_term lthy raw_mapper;
-    val T = fastype_of input_mapper;
-    val _ = Type.no_tvars T;
-    val mapper = singleton (Variable.polymorphic lthy) input_mapper;
-    val _ = if null (Term.add_tfreesT (fastype_of mapper) []) then ()
-      else error ("Illegal locally fixed variables in type: " ^ Syntax.string_of_typ lthy T);
-    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
-      | add_tycos _ = I;
-    val tycos = add_tycos T [];
-    val tyco = if tycos = ["fun"] then "fun"
-      else case remove (op =) "fun" tycos
-       of [tyco] => tyco
-        | _ => error ("Bad number of type constructors: " ^ Syntax.string_of_typ lthy T);
+    val (mapper, T, tyco) = analyze_mapper lthy (prep_term lthy raw_mapper);
     val prfx = the_default (Long_Name.base_name tyco) some_prfx;
     val variances = analyze_variances lthy tyco T;
     val (comp_prop, prove_compositionality) = make_comp_prop lthy variances (tyco, mapper);
@@ -221,8 +236,9 @@
         val typ_instance = Sign.typ_instance (Context.theory_of context);
         val mapper' = Morphism.term phi mapper;
         val T_T' = pairself fastype_of (mapper, mapper');
+        val vars = Term.add_vars mapper' [];
       in
-        if typ_instance T_T' andalso typ_instance (swap T_T')
+        if null vars andalso typ_instance T_T' andalso typ_instance (swap T_T')
         then (Data.map o Symtab.cons_list) (tyco,
           { mapper = mapper', variances = variances,
             comp = Morphism.thm phi comp_thm, id = Morphism.thm phi id_thm }) context

--- a/src/Tools/Code/code_scala.ML	Fri Mar 09 20:04:19 2012 +0100
+++ b/src/Tools/Code/code_scala.ML	Fri Mar 09 22:05:15 2012 +0100
@@ -130,10 +130,11 @@
                 val (p_pat, vars') = print_bind tyvars some_thm NOBR pat vars;
                 val p_body = print_term tyvars false some_thm vars' NOBR body
               in concat [str "case", p_pat, str "=>", p_body] end;
-          in brackify_block fxy
-            (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
-            (map print_select clauses)
-            (str "}")
+          in
+            map print_select clauses
+            |> Pretty.block_enclose (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"], str "}")
+            |> single
+            |> enclose "(" ")"
           end
       | print_case tyvars some_thm vars fxy ((_, []), _) =
           (brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];