97 (* store theorems in theory *) |
97 (* store theorems in theory *) |
98 |
98 |
99 fun store_thmss_atts label tnames attss thmss = |
99 fun store_thmss_atts label tnames attss thmss = |
100 fold_map (fn ((tname, atts), thms) => |
100 fold_map (fn ((tname, atts), thms) => |
101 Sign.add_path tname |
101 Sign.add_path tname |
102 #> PureThy.add_thmss [((Binding.name label, thms), atts)] |
102 #> Global_Theory.add_thmss [((Binding.name label, thms), atts)] |
103 #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) |
103 #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) |
104 ##> Theory.checkpoint; |
104 ##> Theory.checkpoint; |
105 |
105 |
106 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []); |
106 fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []); |
107 |
107 |
108 fun store_thms_atts label tnames attss thmss = |
108 fun store_thms_atts label tnames attss thmss = |
109 fold_map (fn ((tname, atts), thms) => |
109 fold_map (fn ((tname, atts), thms) => |
110 Sign.add_path tname |
110 Sign.add_path tname |
111 #> PureThy.add_thms [((Binding.name label, thms), atts)] |
111 #> Global_Theory.add_thms [((Binding.name label, thms), atts)] |
112 #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) |
112 #-> (fn thm::_ => Sign.parent_path #> pair thm)) (tnames ~~ attss ~~ thmss) |
113 ##> Theory.checkpoint; |
113 ##> Theory.checkpoint; |
114 |
114 |
115 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []); |
115 fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []); |
116 |
116 |