33 val empty = ([],[]) |
33 val empty = ([],[]) |
34 val copy = I; |
34 val copy = I; |
35 val extend = I; |
35 val extend = I; |
36 |
36 |
37 fun merge _ ((pres1,posts1), (pres2,posts2)) = |
37 fun merge _ ((pres1,posts1), (pres2,posts2)) = |
38 (Library.merge eq_thm (pres1,pres2), Library.merge eq_thm (posts1,posts2)) |
38 (Library.merge Thm.eq_thm (pres1,pres2), Library.merge Thm.eq_thm (posts1,posts2)) |
39 |
39 |
40 fun print _ _ = () |
40 fun print _ _ = () |
41 end); |
41 end); |
42 |
42 |
43 val _ = |
43 val _ = |
44 let |
44 let |
45 fun map_data f = Context.mapping (NBE_Rewrite.map f) I; |
45 fun map_data f = Context.mapping (NBE_Rewrite.map f) I; |
46 fun attr_pre (thy, thm) = |
46 fun attr_pre (thy, thm) = |
47 ((map_data o apfst) (insert eq_thm thm) thy, thm) |
47 ((map_data o apfst) (insert Thm.eq_thm thm) thy, thm) |
48 fun attr_post (thy, thm) = |
48 fun attr_post (thy, thm) = |
49 ((map_data o apsnd) (insert eq_thm thm) thy, thm) |
49 ((map_data o apsnd) (insert Thm.eq_thm thm) thy, thm) |
50 val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre |
50 val attr = Attrib.syntax (Scan.lift (Args.$$$ "pre" >> K attr_pre |
51 || Args.$$$ "post" >> K attr_post)); |
51 || Args.$$$ "post" >> K attr_post)); |
52 in |
52 in |
53 Context.add_setup ( |
53 Context.add_setup ( |
54 NBE_Rewrite.init |
54 NBE_Rewrite.init |