equal
deleted
inserted
replaced
240 |
240 |
241 (* Since Isabelle2017 sessions in theory identifiers are enforced. |
241 (* Since Isabelle2017 sessions in theory identifiers are enforced. |
242 However, we leave theory identifiers short, in particular in use as keys into KEStore. *) |
242 However, we leave theory identifiers short, in particular in use as keys into KEStore. *) |
243 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID) |
243 fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID) |
244 |
244 |
|
245 fun thm2str thm = |
|
246 let |
|
247 val t = Thm.prop_of thm |
|
248 val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac")) |
|
249 val ctxt' = Config.put show_markup false ctxt |
|
250 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
|
251 |
245 fun term_to_string' ctxt t = |
252 fun term_to_string' ctxt t = |
246 let |
253 let |
247 val ctxt' = Config.put show_markup false ctxt |
254 val ctxt' = Config.put show_markup false ctxt |
248 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
255 in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end; |
249 fun term_to_string'' (thyID : thyID) t = |
256 fun term_to_string'' (thyID : thyID) t = |