--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Sep 20 18:42:56 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Sep 20 18:43:39 2005 +0200
@@ -130,8 +130,7 @@
(Pretty.setmp_margin 999 string_of_thm));
fun fake_thm_name th =
- Context.theory_name (theory_of_thm th) ^ "." ^
- ResLib.trim_ends (plain_string_of_thm th);
+ Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th);
fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
else ("HOL.TrueI",TrueI)