src/Pure/Isar/local_defs.ML

 fun trans_list _ _ [] = raise Empty
   | trans_list trans ctxt (th :: raw_eqs) =
       (case filter_out is_trivial raw_eqs of
         [] => th
       | eqs =>
-          let val ((_, th' :: eqs'), ctxt') = Variable.import_thms true (th :: eqs) ctxt
+          let val ((_, th' :: eqs'), ctxt') = Variable.import true (th :: eqs) ctxt
           in singleton (Variable.export ctxt' ctxt) (fold trans eqs' th') end);
 
 in
 
 val trans_terms = trans_list (fn eq2 => fn eq1 => eq2 COMP (eq1 COMP Drule.transitive_thm));