equal
deleted
inserted
replaced
105 val _ = |
105 val _ = |
106 let |
106 let |
107 val code_attr = Attrib.syntax (Scan.peek (fn context => |
107 val code_attr = Attrib.syntax (Scan.peek (fn context => |
108 List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))))); |
108 List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))))); |
109 in |
109 in |
110 Context.add_setup (Attrib.add_attributes |
110 Context.>> (Attrib.add_attributes |
111 [("code", code_attr, "declare theorems for code generation")]) |
111 [("code", code_attr, "declare theorems for code generation")]) |
112 end; |
112 end; |
113 |
113 |
114 |
114 |
115 (** certificate theorems **) |
115 (** certificate theorems **) |
385 val data2' = invoke_purge_all NONE touched (! data2); |
385 val data2' = invoke_purge_all NONE touched (! data2); |
386 val data = invoke_merge_all pp (data1', data2'); |
386 val data = invoke_merge_all pp (data1', data2'); |
387 in (exec, ref data) end; |
387 in (exec, ref data) end; |
388 ); |
388 ); |
389 |
389 |
390 val _ = Context.add_setup CodeData.init; |
390 val _ = Context.>> CodeData.init; |
391 |
391 |
392 fun thy_data f thy = f ((snd o CodeData.get) thy); |
392 fun thy_data f thy = f ((snd o CodeData.get) thy); |
393 |
393 |
394 fun get_ensure_init kind data_ref = |
394 fun get_ensure_init kind data_ref = |
395 case Datatab.lookup (! data_ref) kind |
395 case Datatab.lookup (! data_ref) kind |
862 fun del_post thm thy = |
862 fun del_post thm thy = |
863 (map_exec_purge NONE o map_thmproc o apsnd) |
863 (map_exec_purge NONE o map_thmproc o apsnd) |
864 (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy; |
864 (remove Thm.eq_thm_prop (CodeUnit.error_thm CodeUnit.mk_rew thm)) thy; |
865 (*fully applied in order to get right context for mk_rew!*) |
865 (*fully applied in order to get right context for mk_rew!*) |
866 |
866 |
867 val _ = Context.add_setup |
867 val _ = Context.>> |
868 (let |
868 (let |
869 fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); |
869 fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); |
870 fun add_simple_attribute (name, f) = |
870 fun add_simple_attribute (name, f) = |
871 add_attribute (name, Scan.succeed (mk_attribute f)); |
871 add_attribute (name, Scan.succeed (mk_attribute f)); |
872 fun add_del_attribute (name, (add, del)) = |
872 fun add_del_attribute (name, (add, del)) = |