# HG changeset patch
# User haftmann
# Date 1334776310 -7200
# Node ID 978bd14ad0658fea7678e6b14b73adcf1be63bfd
# Parent  10c92d6a3caf62af11e5a57e27ed8fde97d5c018
tuned

diff -r 10c92d6a3caf -r 978bd14ad065 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Wed Apr 18 20:48:15 2012 +0200
+++ b/src/Pure/Isar/code.ML	Wed Apr 18 21:11:50 2012 +0200
@@ -948,12 +948,12 @@
                       :: Pretty.str "of"
                       :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
       );
-    fun ignored_cases NONE = "<ignored>"
-      | ignored_cases (SOME c) = string_of_const thy c
+    fun pretty_caseparam NONE = "<ignored>"
+      | pretty_caseparam (SOME c) = string_of_const thy c
     fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
       | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
           Pretty.str (string_of_const thy const), Pretty.str "with",
-          (Pretty.block o Pretty.commas o map (Pretty.str o ignored_cases)) cos];
+          (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
     val functions = the_functions exec
       |> Symtab.dest
       |> (map o apsnd) (snd o fst)
@@ -1089,7 +1089,7 @@
 fun add_case thm thy =
   let
     val (case_const, (k, cos)) = case_cert thm;
-    val _ = case map_filter I cos |> filter_out (is_constr thy)
+    val _ = case (filter_out (is_constr thy) o map_filter I) cos
      of [] => ()
       | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
     val entry = (1 + Int.max (1, length cos), (k, cos));
diff -r 10c92d6a3caf -r 978bd14ad065 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Apr 18 20:48:15 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Apr 18 21:11:50 2012 +0200
@@ -580,19 +580,20 @@
       (err_typ ^ "\n" ^ err_class)
   end;
 
+
 (* inference of type annotations for disambiguation with type classes *)
 
 fun mk_tagged_type (true, T) = Type ("", [T])
-  | mk_tagged_type (false, T) = T
+  | mk_tagged_type (false, T) = T;
 
 fun dest_tagged_type (Type ("", [T])) = (true, T)
-  | dest_tagged_type T = (false, T)
+  | dest_tagged_type T = (false, T);
 
-val untag_term = map_types (snd o dest_tagged_type)
+val untag_term = map_types (snd o dest_tagged_type);
 
 fun tag_term (proj_sort, _) eqngr =
   let
-    val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
+    val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
     fun tag (Const (c', T')) (Const (c, T)) =
         Const (c,
           mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
@@ -600,7 +601,7 @@
       | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
       | tag (Free _) (t as Free _) = t
       | tag (Var _) (t as Var _) = t
-      | tag (Bound _) (t as Bound _) = t
+      | tag (Bound _) (t as Bound _) = t;
   in
     tag
   end
@@ -620,6 +621,7 @@
   map (apfst (fn (args, (rhs, some_abs)) => (args,
     (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
 
+
 (* translation *)
 
 fun ensure_tyco thy algbr eqngr permissive tyco =
@@ -782,13 +784,13 @@
     val tys = arg_types num_args (snd c_ty);
     val ty = nth tys t_pos;
     fun mk_constr NONE t = NONE
-      | mk_constr (SOME c) t = let val n = Code.args_number thy c
-        in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
-
-    val constrs = if null case_pats then []
-      else map2 mk_constr case_pats (nth_drop t_pos ts);
-    val constrs' = map_filter I constrs
-
+      | mk_constr (SOME c) t =
+          let
+            val n = Code.args_number thy c;
+          in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
+    val constrs =
+      if null case_pats then []
+      else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
     fun casify naming constrs ty ts =
       let
         val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
@@ -821,12 +823,13 @@
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
-              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause)));
+              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
+                (case_pats ~~ ts_clause)));
       in ((t, ty), clauses) end;
   in
     translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
     ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
-      #>> rpair n) constrs'
+      #>> rpair n) constrs
     ##>> translate_typ thy algbr eqngr permissive ty
     ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
     #-> (fn (((t, constrs), ty), ts) =>