src/Tools/nbe.ML

           |> map (Logic.dest_of_class #> of_class);
       in fold Thm.elim_implies prems_of_class thm end;
   in
     ct
     |> (Drule.cterm_fun o map_types o map_type_tfree)
-        (fn (v, sort) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
+        (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     |> conv
     |> Thm.strip_shyps
     |> Thm.varifyT_global
     |> Thm.unconstrainT
     |> instantiate

 val put_result = Univs.put;
 
 local
   val prefix =     "Nbe.";
   val name_put =   prefix ^ "put_result";
-  val name_ref =   prefix ^ "univs_ref";
   val name_const = prefix ^ "Const";
   val name_abss =  prefix ^ "abss";
   val name_apps =  prefix ^ "apps";
   val name_same =  prefix ^ "same";
 in