equal
deleted
inserted
replaced
142 let |
142 let |
143 val eqs = filter (snd o snd) raw_eqs; |
143 val eqs = filter (snd o snd) raw_eqs; |
144 val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; |
144 val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; |
145 fun pr_eq ((ts, t), (thm, _)) = |
145 fun pr_eq ((ts, t), (thm, _)) = |
146 let |
146 let |
147 val consts = map_filter |
147 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
148 (fn c => if (is_some o syntax_const) c |
|
149 then NONE else (SOME o Long_Name.base_name o deresolve) c) |
|
150 (fold Code_Thingol.add_constnames (t :: ts) []); |
|
151 val vars = init_syms |
148 val vars = init_syms |
152 |> Code_Printer.intro_vars consts |
149 |> Code_Printer.intro_base_names |
|
150 (is_none o syntax_const) deresolve consts |
153 |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames) |
151 |> Code_Printer.intro_vars ((fold o Code_Thingol.fold_varnames) |
154 (insert (op =)) ts []); |
152 (insert (op =)) ts []); |
155 in |
153 in |
156 semicolon ( |
154 semicolon ( |
157 (str o deresolve_base) name |
155 (str o deresolve_base) name |