tidied
authorpaulson
Wed Jul 13 15:05:48 2005 +0200 (2005-07-13)
changeset 1679412d00dab5301
parent 16793 51600bfac176
child 16795 b400b53d8f7d
tidied
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_clause.ML	Wed Jul 13 14:56:00 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Jul 13 15:05:48 2005 +0200
     1.3 @@ -645,13 +645,7 @@
     1.4  	cls_str :: (typ_clss 0 tfree_lits)
     1.5      end;
     1.6  
     1.7 -fun clause_info cls =
     1.8 -    let 
     1.9 -	val cls_id = string_of_clauseID cls
    1.10 -	val ax_name = string_of_axiomName cls
    1.11 -    in 
    1.12 -	((ax_name^""), cls_id)
    1.13 -    end;
    1.14 +fun clause_info cls = (string_of_axiomName cls, string_of_clauseID cls);
    1.15  
    1.16  
    1.17  fun clause2tptp cls =