changeset 20854 | f9cf9e62d11c |
parent 20824 | aca7d38283bf |
child 21254 | d53f76357f41 |
--- a/src/HOL/Tools/res_clause.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Oct 04 14:17:38 2006 +0200 @@ -452,7 +452,7 @@ 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*)