src/HOL/Tools/res_clause.ML

                   kind = kind, literals = lits, types_sorts = types_sorts}
   end;		     
 
 fun get_tvar_strs [] = []
   | get_tvar_strs ((FOLTVar indx,s)::tss) = 
-      (make_schematic_type_var indx) ins (get_tvar_strs tss)
+      insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
   | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
 
 (* check if a clause is first-order before making a conjecture clause*)
 fun make_conjecture_clause n th =
   if Meson.is_fol_term (prop_of th) then make_clause(n, "conjecture", th, Conjecture)