1.1 --- a/src/Tools/isac/calcelems.sml	Tue Jun 25 16:21:18 2019 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Wed Jul 03 15:09:16 2019 +0200
     1.3 @@ -108,7 +108,6 @@
     1.4      val thm''_of_thm: thm -> thm''
     1.5      val thm_of_thm: Rule.rule -> thm
     1.6  (* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)
     1.7 -    val thm2str: thm -> string
     1.8      val pats2str' : pat list -> string
     1.9      val insert_fillpats: thydata ptyp list -> (pblID * fillpat list) list -> thydata ptyp list ->
    1.10        thydata ptyp list
    1.11 @@ -213,13 +212,6 @@
    1.12      # ???
    1.13  *)
    1.14  
    1.15 -fun thm2str thm =
    1.16 -  let
    1.17 -    val t = Thm.prop_of thm
    1.18 -    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac"))
    1.19 -    val ctxt' = Config.put show_markup false ctxt
    1.20 -  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;
    1.21 -                 
    1.22  fun id_of_thm (Rule.Thm (id, _)) = id  (* TODO re-arrange code for rule2str *)
    1.23    | id_of_thm _ = raise ERROR ("id_of_thm: uncovered case " (* ^ rule2str r *))
    1.24  fun thm_of_thm (Rule.Thm (_, thm)) = thm  (* TODO re-arrange code for rule2str *)