src/Provers/hypsubst.ML
changeset 45659 09539cdffcd7
parent 45625 750c5a47400b
child 46219 426ed18eba43
equal deleted inserted replaced
45658:c2c647a4c237 45659:09539cdffcd7
   137       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   137       end handle THM _ => no_tac | EQ_VAR => no_tac) i st
   138     in REPEAT_DETERM1 o tac end;
   138     in REPEAT_DETERM1 o tac end;
   139 
   139 
   140 end;
   140 end;
   141 
   141 
   142 val ssubst = Drule.export_without_context (Data.sym RS Data.subst);
   142 val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
   143 
   143 
   144 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   144 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   145   case try (Logic.strip_assums_hyp #> hd #>
   145   case try (Logic.strip_assums_hyp #> hd #>
   146       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   146       Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
   147     SOME (t, t') =>
   147     SOME (t, t') =>