158 let |
158 let |
159 val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); |
159 val (bind :: binds, body) = Code_Thingol.unfold_let (ICase case_expr); |
160 fun print_match_val ((pat, ty), t) vars = |
160 fun print_match_val ((pat, ty), t) vars = |
161 vars |
161 vars |
162 |> print_bind tyvars some_thm BR pat |
162 |> print_bind tyvars some_thm BR pat |
163 |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), |
163 |>> (fn p => (false, concat [str "val", p, str "=", |
164 str "=", print_term tyvars false some_thm vars NOBR t])); |
164 constraint (print_term tyvars false some_thm vars NOBR t) (print_typ tyvars NOBR ty)])); |
165 fun print_match_seq t vars = |
165 fun print_match_seq t vars = |
166 ((true, print_term tyvars false some_thm vars NOBR t), vars); |
166 ((true, print_term tyvars false some_thm vars NOBR t), vars); |
167 fun print_match is_first ((IVar NONE, ty), t) = |
167 fun print_match is_first ((IVar NONE, ty), t) = |
168 if Code_Thingol.is_IAbs t andalso is_first |
168 if Code_Thingol.is_IAbs t andalso is_first |
169 then print_match_val ((IVar NONE, ty), t) |
169 then print_match_val ((IVar NONE, ty), t) |