1.1 --- a/src/Tools/isac/calcelems.sml	Mon Apr 20 10:27:19 2015 +0200
     1.2 +++ b/src/Tools/isac/calcelems.sml	Mon Apr 20 10:33:55 2015 +0200
     1.3 @@ -292,6 +292,7 @@
     1.4  
     1.5  (*check for [.] as caused by "fun assoc_thm'"*)
     1.6  fun string_of_thm thm = term_to_string' (thy2ctxt' "Isac") (prop_of thm)
     1.7 +fun string_of_thm' thy thm = term_to_string' (thy2ctxt thy) (prop_of thm)
     1.8  fun string_of_thmI thm =
     1.9    let 
    1.10      val str = (de_quote o string_of_thm) thm