1.1 --- a/src/Pure/Isar/code.ML	Wed Apr 18 20:48:15 2012 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Apr 18 21:11:50 2012 +0200
     1.3 @@ -948,12 +948,12 @@
     1.4                        :: Pretty.str "of"
     1.5                        :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
     1.6        );
     1.7 -    fun ignored_cases NONE = "<ignored>"
     1.8 -      | ignored_cases (SOME c) = string_of_const thy c
     1.9 +    fun pretty_caseparam NONE = "<ignored>"
    1.10 +      | pretty_caseparam (SOME c) = string_of_const thy c
    1.11      fun pretty_case (const, ((_, (_, [])), _)) = Pretty.str (string_of_const thy const)
    1.12        | pretty_case (const, ((_, (_, cos)), _)) = (Pretty.block o Pretty.breaks) [
    1.13            Pretty.str (string_of_const thy const), Pretty.str "with",
    1.14 -          (Pretty.block o Pretty.commas o map (Pretty.str o ignored_cases)) cos];
    1.15 +          (Pretty.block o Pretty.commas o map (Pretty.str o pretty_caseparam)) cos];
    1.16      val functions = the_functions exec
    1.17        |> Symtab.dest
    1.18        |> (map o apsnd) (snd o fst)
    1.19 @@ -1089,7 +1089,7 @@
    1.20  fun add_case thm thy =
    1.21    let
    1.22      val (case_const, (k, cos)) = case_cert thm;
    1.23 -    val _ = case map_filter I cos |> filter_out (is_constr thy)
    1.24 +    val _ = case (filter_out (is_constr thy) o map_filter I) cos
    1.25       of [] => ()
    1.26        | cs => error ("Non-constructor(s) in case certificate: " ^ commas_quote cs);
    1.27      val entry = (1 + Int.max (1, length cos), (k, cos));

     2.1 --- a/src/Tools/Code/code_thingol.ML	Wed Apr 18 20:48:15 2012 +0200
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Apr 18 21:11:50 2012 +0200
     2.3 @@ -580,19 +580,20 @@
     2.4        (err_typ ^ "\n" ^ err_class)
     2.5    end;
     2.6  
     2.7 +
     2.8  (* inference of type annotations for disambiguation with type classes *)
     2.9  
    2.10  fun mk_tagged_type (true, T) = Type ("", [T])
    2.11 -  | mk_tagged_type (false, T) = T
    2.12 +  | mk_tagged_type (false, T) = T;
    2.13  
    2.14  fun dest_tagged_type (Type ("", [T])) = (true, T)
    2.15 -  | dest_tagged_type T = (false, T)
    2.16 +  | dest_tagged_type T = (false, T);
    2.17  
    2.18 -val untag_term = map_types (snd o dest_tagged_type)
    2.19 +val untag_term = map_types (snd o dest_tagged_type);
    2.20  
    2.21  fun tag_term (proj_sort, _) eqngr =
    2.22    let
    2.23 -    val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
    2.24 +    val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
    2.25      fun tag (Const (c', T')) (Const (c, T)) =
    2.26          Const (c,
    2.27            mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
    2.28 @@ -600,7 +601,7 @@
    2.29        | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
    2.30        | tag (Free _) (t as Free _) = t
    2.31        | tag (Var _) (t as Var _) = t
    2.32 -      | tag (Bound _) (t as Bound _) = t
    2.33 +      | tag (Bound _) (t as Bound _) = t;
    2.34    in
    2.35      tag
    2.36    end
    2.37 @@ -620,6 +621,7 @@
    2.38    map (apfst (fn (args, (rhs, some_abs)) => (args,
    2.39      (annotate thy algbr eqngr (c, ty) args rhs, some_abs)))) eqns
    2.40  
    2.41 +
    2.42  (* translation *)
    2.43  
    2.44  fun ensure_tyco thy algbr eqngr permissive tyco =
    2.45 @@ -782,13 +784,13 @@
    2.46      val tys = arg_types num_args (snd c_ty);
    2.47      val ty = nth tys t_pos;
    2.48      fun mk_constr NONE t = NONE
    2.49 -      | mk_constr (SOME c) t = let val n = Code.args_number thy c
    2.50 -        in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
    2.51 -
    2.52 -    val constrs = if null case_pats then []
    2.53 -      else map2 mk_constr case_pats (nth_drop t_pos ts);
    2.54 -    val constrs' = map_filter I constrs
    2.55 -
    2.56 +      | mk_constr (SOME c) t =
    2.57 +          let
    2.58 +            val n = Code.args_number thy c;
    2.59 +          in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
    2.60 +    val constrs =
    2.61 +      if null case_pats then []
    2.62 +      else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
    2.63      fun casify naming constrs ty ts =
    2.64        let
    2.65          val undefineds = map_filter (lookup_const naming) (Code.undefineds thy);
    2.66 @@ -821,12 +823,13 @@
    2.67            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
    2.68            else maps (fn ((constr as IConst (_, ((_, (tys, _)), _)), n), t) =>
    2.69              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
    2.70 -              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t) (case_pats ~~ ts_clause)));
    2.71 +              (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
    2.72 +                (case_pats ~~ ts_clause)));
    2.73        in ((t, ty), clauses) end;
    2.74    in
    2.75      translate_const thy algbr eqngr permissive some_thm (c_ty, NONE)
    2.76      ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr permissive some_thm (constr, NONE)
    2.77 -      #>> rpair n) constrs'
    2.78 +      #>> rpair n) constrs
    2.79      ##>> translate_typ thy algbr eqngr permissive ty
    2.80      ##>> fold_map (translate_term thy algbr eqngr permissive some_thm o rpair NONE) ts
    2.81      #-> (fn (((t, constrs), ty), ts) =>