src/HOL/Tools/ATP/res_clasimpset.ML
changeset 17525 ae5bb6001afb
parent 17484 f6a225f97f0a
child 17596 cd555d5a3254
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Sep 20 18:42:56 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Sep 20 18:43:39 2005 +0200
     1.3 @@ -130,8 +130,7 @@
     1.4  	(Pretty.setmp_margin 999 string_of_thm));
     1.5  	
     1.6  fun fake_thm_name th = 
     1.7 -    Context.theory_name (theory_of_thm th) ^ "." ^ 
     1.8 -    ResLib.trim_ends (plain_string_of_thm th);
     1.9 +    Context.theory_name (theory_of_thm th) ^ "." ^ unenclose (plain_string_of_thm th);
    1.10  
    1.11  fun put_name_pair ("",th) = if !use_nameless then (fake_thm_name th, th)
    1.12                              else ("HOL.TrueI",TrueI)