equal
deleted
inserted
replaced
123 |
123 |
124 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
124 val info = { add_simps=addsmps, case_names=cnames, psimps=psimps', |
125 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
125 pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination', |
126 fs=fs, R=R, defname=defname, is_partial=true } |
126 fs=fs, R=R, defname=defname, is_partial=true } |
127 |
127 |
128 val _ = |
128 val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes) |
129 if not is_external then () |
|
130 else Specification.print_consts lthy (K false) (map fst fixes) |
|
131 in |
129 in |
132 (info, |
130 (info, |
133 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
131 lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info)) |
134 end |
132 end |
135 in |
133 in |