src/Provers/ind.ML

--- a/src/Provers/ind.ML	Wed Oct 04 14:14:33 2006 +0200
+++ b/src/Provers/ind.ML	Wed Oct 04 14:17:38 2006 +0200
@@ -28,7 +28,7 @@
 
 fun add_term_frees thy =
 let fun add(tm, vars) = case tm of
-	Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
+	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
 		     else vars
       | Abs (_,_,body) => add(body,vars)
       | rator$rand => add(rator, add(rand, vars))