src/Provers/hypsubst.ML

       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
     in REPEAT_DETERM1 o tac end;
 
 end;
 
-val ssubst = Drule.standard (Data.sym RS Data.subst);
+val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
 
 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   case try (Logic.strip_assums_hyp #> hd #>
       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
     SOME (t, t') =>