1.1 --- a/src/HOL/Tools/res_clause.ML	Thu May 12 15:42:58 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Thu May 12 18:24:42 2005 +0200
     1.3 @@ -352,16 +352,10 @@
     1.4          val ts'' = ResLib.no_rep_app ts ts' 
     1.5      in
     1.6          (lits',ts'')
     1.7 -    end
     1.8 -  | literals_of_term _ = raise CLAUSE("Unexpected clause format");
     1.9 +    end;
    1.10       
    1.11  
    1.12 -fun literals_of_thm thm = 
    1.13 -    let val term_of_thm = prop_of thm
    1.14 -			  
    1.15 -    in
    1.16 -	literals_of_term (term_of_thm,([],[]))
    1.17 -    end;
    1.18 +fun literals_of_thm thm = literals_of_term (prop_of thm, ([],[]));
    1.19      
    1.20   
    1.21  fun sorts_on_typs (_, []) = []