1.1 --- a/src/FOL/hypsubstdata.ML	Wed Sep 29 10:33:15 2010 +0200
     1.2 +++ b/src/FOL/hypsubstdata.ML	Wed Sep 29 11:36:16 2010 +0200
     1.3 @@ -13,8 +13,6 @@
     1.4    val subst = @{thm subst}
     1.5    val sym = @{thm sym}
     1.6    val thin_refl = @{thm thin_refl}
     1.7 -  val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
     1.8 -                     by (unfold prop_def) (drule eq_reflection, unfold)}
     1.9  end;
    1.10  
    1.11  structure Hypsubst = HypsubstFun(Hypsubst_Data);

     2.1 --- a/src/HOL/HOL.thy	Wed Sep 29 10:33:15 2010 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Sep 29 11:36:16 2010 +0200
     2.3 @@ -834,8 +834,6 @@
     2.4    val subst = @{thm subst}
     2.5    val sym = @{thm sym}
     2.6    val thin_refl = @{thm thin_refl};
     2.7 -  val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)"
     2.8 -                     by (unfold prop_def) (drule eq_reflection, unfold)}
     2.9  end);
    2.10  open Hypsubst;
    2.11  

     3.1 --- a/src/Provers/hypsubst.ML	Wed Sep 29 10:33:15 2010 +0200
     3.2 +++ b/src/Provers/hypsubst.ML	Wed Sep 29 11:36:16 2010 +0200
     3.3 @@ -42,13 +42,10 @@
     3.4    val subst            : thm               (* [| a=b;  P(a) |] ==> P(b) *)
     3.5    val sym              : thm               (* a=b ==> b=a *)
     3.6    val thin_refl        : thm               (* [|x=x; PROP W|] ==> PROP W *)
     3.7 -  val prop_subst       : thm               (* PROP P t ==> PROP prop (x = t ==> PROP P x) *)
     3.8  end;
     3.9  
    3.10  signature HYPSUBST =
    3.11  sig
    3.12 -  val single_hyp_subst_tac   : int -> int -> tactic
    3.13 -  val single_hyp_meta_subst_tac : int -> int -> tactic
    3.14    val bound_hyp_subst_tac    : int -> tactic
    3.15    val hyp_subst_tac          : int -> tactic
    3.16    val blast_hyp_subst_tac    : bool -> int -> tactic
    3.17 @@ -61,27 +58,6 @@
    3.18  
    3.19  exception EQ_VAR;
    3.20  
    3.21 -val meta_subst = @{lemma "PROP P t \<Longrightarrow> PROP prop (x \<equiv> t \<Longrightarrow> PROP P x)"
    3.22 -  by (unfold prop_def)}
    3.23 -
    3.24 -(** Simple version: Just subtitute one hypothesis, specified by index k **)
    3.25 -fun gen_single_hyp_subst_tac subst_rule k = CSUBGOAL (fn (csubg, i) =>
    3.26 - let 
    3.27 -   val pat = fold_rev (Logic.all o Free) (Logic.strip_params (term_of csubg)) (Term.dummy_pattern propT)
    3.28 -             |> cterm_of (theory_of_cterm csubg)
    3.29 -
    3.30 -   val rule =
    3.31 -       Thm.lift_rule pat subst_rule (* lift just over parameters *)
    3.32 -       |> Conv.fconv_rule (MetaSimplifier.rewrite true [@{thm prop_def}])
    3.33 - in
    3.34 -   rotate_tac k i
    3.35 -   THEN Thm.compose_no_flatten false (rule, 1) i
    3.36 -   THEN rotate_tac (~k) i
    3.37 - end)
    3.38 -
    3.39 -val single_hyp_meta_subst_tac = gen_single_hyp_subst_tac meta_subst
    3.40 -val single_hyp_subst_tac = gen_single_hyp_subst_tac Data.prop_subst
    3.41 -
    3.42  fun loose (i,t) = member (op =) (add_loose_bnos (t, i, [])) 0;
    3.43  
    3.44  (*Simplifier turns Bound variables to special Free variables: