1.1 --- a/src/Tools/isac/calcelems.sml	Thu Jul 24 15:18:22 2014 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Thu Jul 24 15:44:50 2014 +0200
     1.3 @@ -278,13 +278,12 @@
     1.4  fun eq_thmI' ((thmid1, _), (thmid2, _)) =
     1.5      (thmID_of_derivation_name thmid1) = (thmID_of_derivation_name thmid2);
     1.6  
     1.7 -val string_of_thm =  Thm.get_name_hint; (*FIXME.2009*)
     1.8  fun thm'_of_thm thm =
     1.9    ((thmID_of_derivation_name o Thm.get_name_hint) thm, ""): thm'
    1.10  
    1.11  (*check for [.] as caused by "fun assoc_thm'"*)
    1.12  fun string_of_thmI thm =
    1.13 -    let val ct' = (de_quote o string_of_thm) thm
    1.14 +    let val ct' = (de_quote o Thm.get_name_hint) thm
    1.15  	val (a, b) = split_nlast (5, Symbol.explode ct')
    1.16      in case b of
    1.17  	   [" ", " ","[", ".", "]"] => implode a