1.1 --- a/src/Tools/isac/calcelems.sml	Thu Jul 24 15:44:50 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jul 24 17:22:21 2014 +0200
     1.3 @@ -282,6 +282,17 @@
     1.4    ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'
     1.5  
     1.6  (*check for [.] as caused by "fun assoc_thm'"*)
     1.7 +fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
     1.8 +fun string_of_thmI thm =
     1.9 +  let 
    1.10 +    val str = (de_quote o string_of_thm) thm
    1.11 +    val (a, b) = split_nlast (5, Symbol.explode str)
    1.12 +  in 
    1.13 +    case b of
    1.14 +      [" ", " ","[", ".", "]"] => implode a
    1.15 +    | _ => str
    1.16 +  end
    1.17 +(*
    1.18  fun string_of_thmI thm =
    1.19      let val ct' = (de_quote o Thm.get_name_hint) thm
    1.20  	val (a, b) = split_nlast (5, Symbol.explode ct')
    1.21 @@ -289,6 +300,7 @@
    1.22  	   [" ", " ","[", ".", "]"] => implode a
    1.23  	 | _ => ct'
    1.24      end;
    1.25 +*)
    1.26  
    1.27  (*.id requested for all, Rls,Seq,Rrls.*)
    1.28  fun id_rls Erls = "e_rls" (*WN060714 quick and dirty: recursive defs!*)