equal
deleted
inserted
replaced
276 in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; |
276 in make_entity_markup (Thm_Name.print (name, i)) (Thm_Name.print (xname, i)) pos serial end; |
277 |
277 |
278 fun encode_thm thm_id raw_thm = |
278 fun encode_thm thm_id raw_thm = |
279 let |
279 let |
280 val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); |
280 val deps = map (Thm_Name.print o #2) (Thm_Deps.thm_deps thy [raw_thm]); |
281 val thm = Thm.unconstrainT (clean_thm raw_thm); |
281 val thm = clean_thm (Thm.unconstrainT raw_thm); |
282 val boxes = proof_boxes_of thm thm_id; |
282 val boxes = proof_boxes_of thm thm_id; |
283 |
283 |
284 val proof0 = |
284 val proof0 = |
285 if export_standard_proofs then |
285 if export_standard_proofs then |
286 Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm |
286 Thm.standard_proof_of {full = true, expand_name = SOME o expand_name thm_id} thm |