(* Title:  CalcElements/thmC.sml

   Author: Walther Neuper

   (c) due to copyright terms

TODO: use "ThmC" for renaming identifiers.

Probably this structure can be dropped due to improvements of Isabelle.

*)

signature THEOREM_ISAC =

sig

(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)

  val string_of_thmI: thm -> string

(* ---- for tests only: shifted from below to remove the Warning "unused" at fun.def. --------- *)

  val thm2str: thm -> string

  val thms2str : thm list -> string

(*/-------------------------------------------------------- ! aktivate for Test_Isac BEGIN ---\* )

  val string_of_thm: thm -> string

  val string_of_thm': theory -> thm -> string

( *\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)

end

(**)

structure ThmC(**): THEOREM_ISAC(**) =

struct

(**)

(*datatype T = Rule_Def.Thm  ..ERROR: cannot get out from Rule_Def.rule*)

fun thm2str thm =

  let

    val t = Thm.prop_of thm

    val ctxt = Proof_Context.init_global (Thy_Info.get_theory ("Isac.Isac_Knowledge"))

    val ctxt' = Config.put show_markup false ctxt

  in Print_Mode.setmp [] (Syntax.string_of_term ctxt') t end;

fun thms2str thms = (strs2str o (map thm2str)) thms

(*check for [.] as caused by "fun assoc_thm'"*)

fun string_of_thm thm = Rule.term_to_string' (ThyC.thy2ctxt' "Isac_Knowledge") (Thm.prop_of thm)

fun string_of_thm' thy thm = Rule.term_to_string' (ThyC.thy2ctxt thy) (Thm.prop_of thm)

fun string_of_thmI thm =

  let 

    val str = (de_quote o string_of_thm) thm

    val (a, b) = split_nlast (5, Symbol.explode str)

  in 

    case b of

      [" ", " ","[", ".", "]"] => implode a

    | _ => str

  end

(**)end(**)