src/HOL/Matrix/Compute_Oracle/linker.ML

         (added_substs, Instances (cfilter, ctab, minsets, substs))
     end
 
 fun substs_of (Instances (_,_,_,substs)) = Substtab.keys substs
 
-fun eq_to_meta th = (@{thm HOL.eq_reflection} OF [th] handle THM _ => th)
-
 
 local
 
-fun collect (Var x) tab = tab
+fun collect (Var _) tab = tab
   | collect (Bound _) tab = tab
   | collect (a $ b) tab = collect b (collect a tab)
   | collect (Abs (_, _, body)) tab = collect body tab
   | collect t tab = Consttab.update (constant_of t, ()) tab