src/Pure/drule.ML

 val forall_elim_vars = PureThy.forall_elim_vars;
 
 fun outer_params t =
   let
     val vs = Term.strip_all_vars t;
-    val clean_name = perhaps (try Syntax.dest_skolem) #> perhaps (try Syntax.dest_internal);
+    val clean_name = perhaps (try Term.dest_skolem) #> perhaps (try Term.dest_internal);
   in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
 fun gen_all th =
   let

 fun tvars_intr_list tfrees thm =
   apfst (map (fn ((s, S), ixn) => (s, (ixn, S)))) (Thm.varifyT'
     (gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
 
 
-(* increment var indexes *)
+(* var indexes *)
 
 fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
 
 fun incr_indexes2 th1 th2 =
   Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);