101 and print_bind tyvars some_thm fxy p = |
101 and print_bind tyvars some_thm fxy p = |
102 gen_print_bind (print_term tyvars true) some_thm fxy p |
102 gen_print_bind (print_term tyvars true) some_thm fxy p |
103 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
103 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
104 let |
104 let |
105 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
105 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
106 fun print_match ((IVar NONE, _), t) vars = |
106 fun print_match ((IVar NONE, _), t as _ `|=> _) vars = |
|
107 ((false, enclose "{" "}" [print_term tyvars false some_thm vars NOBR t]), vars) |
|
108 | print_match ((IVar NONE, _), t) vars = |
107 ((true, print_term tyvars false some_thm vars NOBR t), vars) |
109 ((true, print_term tyvars false some_thm vars NOBR t), vars) |
108 | print_match ((pat, ty), t) vars = |
110 | print_match ((pat, ty), t) vars = |
109 vars |
111 vars |
110 |> print_bind tyvars some_thm BR pat |
112 |> print_bind tyvars some_thm BR pat |
111 |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), |
113 |>> (fn p => (false, concat [str "val", constraint p (print_typ tyvars NOBR ty), |