equal
deleted
inserted
replaced
154 let |
154 let |
155 val NominalFunctionResult {fs, R, psimps, simple_pinducts, |
155 val NominalFunctionResult {fs, R, psimps, simple_pinducts, |
156 termination, domintros, cases, eqvts, ...} = |
156 termination, domintros, cases, eqvts, ...} = |
157 cont (Thm.close_derivation proof) |
157 cont (Thm.close_derivation proof) |
158 |
158 |
159 val _ = tracing ("final psimps:\n" ^ cat_lines (map @{make_string} psimps)) |
|
160 val _ = tracing ("final eqvts:\n" ^ cat_lines (map @{make_string} eqvts)) |
|
161 |
|
162 val fnames = map (fst o fst) fixes |
159 val fnames = map (fst o fst) fixes |
163 fun qualify n = Binding.name n |
160 fun qualify n = Binding.name n |
164 |> Binding.qualify true defname |
161 |> Binding.qualify true defname |
165 val conceal_partial = if partials then I else Binding.conceal |
162 val conceal_partial = if partials then I else Binding.conceal |
166 |
163 |
182 |
179 |
183 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
184 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
185 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
186 |
183 |
187 val _ = tracing ("final final psimps:\n" ^ cat_lines (map @{make_string} psimps')) |
|
188 |
|
189 val _ = |
184 val _ = |
190 if not is_external then () |
185 if not is_external then () |
191 else Specification.print_consts lthy (K false) (map fst fixes) |
186 else Specification.print_consts lthy (K false) (map fst fixes) |
192 in |
187 in |
193 (info, |
188 (info, |