src/HOL/List.thy
changeset 55148 7e1b7cb54114
parent 55147 bce3dbc11f95
child 55404 5cb95b79a51f
     1.1 --- a/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -6304,7 +6304,7 @@
     1.4  
     1.5  signature LIST_CODE =
     1.6  sig
     1.7 -  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
     1.8 +  val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option
     1.9    val default_list: int * string
    1.10      -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
    1.11      -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
    1.12 @@ -6316,16 +6316,13 @@
    1.13  
    1.14  open Basic_Code_Thingol;
    1.15  
    1.16 -fun implode_list nil' cons' t =
    1.17 +fun implode_list t =
    1.18    let
    1.19 -    fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    1.20 -          if c = cons'
    1.21 -          then SOME (t1, t2)
    1.22 -          else NONE
    1.23 +    fun dest_cons (IConst { sym = Code_Symbol.Constant @{const_name Cons}, ... } `$ t1 `$ t2) = SOME (t1, t2)
    1.24        | dest_cons _ = NONE;
    1.25      val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    1.26    in case t'
    1.27 -   of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
    1.28 +   of IConst { sym = Code_Symbol.Constant @{const_name Nil}, ... } => SOME ts
    1.29      | _ => NONE
    1.30    end;
    1.31  
    1.32 @@ -6338,15 +6335,15 @@
    1.33  
    1.34  fun add_literal_list target =
    1.35    let
    1.36 -    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
    1.37 -      case Option.map (cons t1) (implode_list nil' cons' t2)
    1.38 +    fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
    1.39 +      case Option.map (cons t1) (implode_list t2)
    1.40         of SOME ts =>
    1.41              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    1.42          | NONE =>
    1.43              default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.44    in
    1.45      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
    1.46 -      [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
    1.47 +      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    1.48    end
    1.49  
    1.50  end;