src/HOL/List.thy
changeset 28708 a1a436f09ec6
parent 28663 bd8438543bf2
child 28789 5a404273ea8f
     1.1 --- a/src/HOL/List.thy	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -3578,7 +3578,7 @@
     1.4  fun pretty_list literals =
     1.5    let
     1.6      val mk_list = Code_Printer.literal_list literals;
     1.7 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
     1.8 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
     1.9        case Option.map (cons t1) (implode_list (list_names naming) t2)
    1.10         of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
    1.11          | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.12 @@ -3589,7 +3589,7 @@
    1.13      val mk_list = Code_Printer.literal_list literals;
    1.14      val mk_char = Code_Printer.literal_char literals;
    1.15      val mk_string = Code_Printer.literal_string literals;
    1.16 -    fun pretty pr naming thm pat vars fxy [(t1, _), (t2, _)] =
    1.17 +    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
    1.18        case Option.map (cons t1) (implode_list (list_names naming) t2)
    1.19         of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
    1.20             of SOME p => p
    1.21 @@ -3600,7 +3600,7 @@
    1.22  fun pretty_char literals =
    1.23    let
    1.24      val mk_char = Code_Printer.literal_char literals;
    1.25 -    fun pretty _ naming thm _ _ _ [(t1, _), (t2, _)] =
    1.26 +    fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
    1.27        case decode_char (nibble_names naming) (t1, t2)
    1.28         of SOME c => (Code_Printer.str o mk_char) c
    1.29          | NONE => Code_Printer.nerror thm "Illegal character expression";
    1.30 @@ -3610,7 +3610,7 @@
    1.31    let
    1.32      val mk_char = Code_Printer.literal_char literals;
    1.33      val mk_string = Code_Printer.literal_string literals;
    1.34 -    fun pretty _ naming thm _ _ _ [(t, _)] =
    1.35 +    fun pretty _ naming thm _ _ [(t, _)] =
    1.36        case implode_list (list_names naming) t
    1.37         of SOME ts => (case implode_string (char_name naming, nibble_names naming) mk_char mk_string ts
    1.38             of SOME p => p