1.1 --- a/src/Tools/isac/calcelems.sml	Sun Feb 25 14:02:42 2018 +0100
     1.2 +++ b/src/Tools/isac/calcelems.sml	Sun Feb 25 16:31:17 2018 +0100
     1.3 @@ -242,6 +242,13 @@
     1.4    However, we leave theory identifiers short, in particular in use as keys into KEStore. *)
     1.5  fun Thy_Info_get_theory thyID = Thy_Info.get_theory ("Isac." ^ thyID)
     1.6       
     1.7 +fun thm2str thm =
     1.8 +  let
     1.9 +    val t = Thm.prop_of thm
    1.10 +    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
    1.11 +    val ctxt' = Config.put show_markup false ctxt
    1.12 +  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    1.13 +
    1.14  fun term_to_string' ctxt t =
    1.15    let
    1.16      val ctxt' = Config.put show_markup false ctxt