306 end; |
306 end; |
307 |
307 |
308 fun thy_note ((name, atts), thms) = |
308 fun thy_note ((name, atts), thms) = |
309 PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); |
309 PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); |
310 fun thy_def false ((name, atts), t) = |
310 fun thy_def false ((name, atts), t) = |
311 PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)) |
311 PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)) |
312 | thy_def true ((name, atts), t) = |
312 | thy_def true ((name, atts), t) = |
313 PureThy.add_defs_unchecked_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); |
313 PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); |
314 |
314 |
315 in |
315 in |
316 |
316 |
317 val add_primrec = gen_primrec thy_note (thy_def false); |
317 val add_primrec = gen_primrec thy_note (thy_def false); |
318 val add_primrec_unchecked = gen_primrec thy_note (thy_def true); |
318 val add_primrec_unchecked = gen_primrec thy_note (thy_def true); |