equal
deleted
inserted
replaced
179 |
179 |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
180 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
181 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
182 fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts} |
183 |
183 |
184 val _ = |
184 val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes) |
185 if not is_external then () |
|
186 else Specification.print_consts lthy (K false) (map fst fixes) |
|
187 in |
185 in |
188 (info, |
186 (info, |
189 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
187 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
190 end |
188 end |
191 in |
189 in |