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 _ = Proof_Display.print_consts do_print |
184 val _ = Proof_Display.print_consts do_print |
185 (Position.thread_data ()) lthy (K false) (map fst fixes) |
185 (Position.thread_data ()) lthy (K false) (map fst fixes) |
186 in |
186 in |
187 (info, |
187 (info, |
188 lthy |> Local_Theory.declaration {syntax = false, pervasive = false} |
188 lthy |> Local_Theory.declaration {syntax = false, pervasive = false} |
189 (add_function_data o morph_function_data info)) |
189 (add_function_data o morph_function_data info)) |
263 || (Parse.reserved "domintros" >> K DomIntros) |
263 || (Parse.reserved "domintros" >> K DomIntros) |
264 || (Parse.reserved "no_partials" >> K No_Partials) |
264 || (Parse.reserved "no_partials" >> K No_Partials) |
265 || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) |
265 || ((Parse.reserved "invariant" |-- Parse.term) >> Invariant)) |
266 |
266 |
267 fun config_parser default = |
267 fun config_parser default = |
268 (Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 option_parser) --| Parse.$$$ ")") []) |
268 (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) |
269 >> (fn opts => fold apply_opt opts default) |
269 >> (fn opts => fold apply_opt opts default) |
270 in |
270 in |
271 fun nominal_function_parser default_cfg = |
271 fun nominal_function_parser default_cfg = |
272 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
272 config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs |
273 end |
273 end |