src/Tools/Code/code_haskell.ML
changeset 55148 7e1b7cb54114
parent 55147 bce3dbc11f95
child 55150 0940309ed8f1
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -432,14 +432,14 @@
     1.4       of SOME ((pat, ty), t') =>
     1.5            SOME ((SOME ((pat, ty), true), t1), t')
     1.6        | NONE => NONE;
     1.7 -    fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
     1.8 -          if c = c_bind_name then dest_bind t1 t2
     1.9 +    fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    1.10 +          if c = c_bind then dest_bind t1 t2
    1.11            else NONE
    1.12 -      | dest_monad _ t = case Code_Thingol.split_let t
    1.13 +      | dest_monad t = case Code_Thingol.split_let t
    1.14           of SOME (((pat, ty), tbind), t') =>
    1.15                SOME ((SOME ((pat, ty), false), tbind), t')
    1.16            | NONE => NONE;
    1.17 -    fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
    1.18 +    val implode_monad = Code_Thingol.unfoldr dest_monad;
    1.19      fun print_monad print_bind print_term (NONE, t) vars =
    1.20            (semicolon [print_term vars NOBR t], vars)
    1.21        | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
    1.22 @@ -448,9 +448,9 @@
    1.23        | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
    1.24            |> print_bind NOBR bind
    1.25            |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
    1.26 -    fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    1.27 +    fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    1.28       of SOME (bind, t') => let
    1.29 -          val (binds, t'') = implode_monad c_bind' t'
    1.30 +          val (binds, t'') = implode_monad t'
    1.31            val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
    1.32              (bind :: binds) vars;
    1.33          in
    1.34 @@ -459,7 +459,7 @@
    1.35          end
    1.36        | NONE => brackify_infix (1, L) fxy
    1.37            (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
    1.38 -  in (2, ([c_bind], pretty)) end;
    1.39 +  in (2, pretty) end;
    1.40  
    1.41  fun add_monad target' raw_c_bind thy =
    1.42    let