1.1 --- a/src/Provers/hypsubst.ML	Fri Jul 04 16:50:57 2014 +0200
     1.2 +++ b/src/Provers/hypsubst.ML	Fri Jul 04 17:19:03 2014 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4  sig
     1.5    val bound_hyp_subst_tac    : Proof.context -> int -> tactic
     1.6    val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
     1.7 -  val hyp_subst_thins        : bool Config.T
     1.8 +  val hyp_subst_thin         : bool Config.T
     1.9    val hyp_subst_tac          : Proof.context -> int -> tactic
    1.10    val blast_hyp_subst_tac    : bool -> int -> tactic
    1.11    val stac                   : thm -> int -> tactic
    1.12 @@ -228,11 +228,11 @@
    1.13      gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
    1.14      if thin then thin_free_eq_tac else K no_tac];
    1.15  
    1.16 -val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool
    1.17 +val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
    1.18      @{binding hypsubst_thin} (K false);
    1.19  
    1.20  fun hyp_subst_tac ctxt = hyp_subst_tac_thin
    1.21 -    (Config.get ctxt hyp_subst_thins) ctxt
    1.22 +    (Config.get ctxt hyp_subst_thin) ctxt
    1.23  
    1.24  (*Substitutes for Bound variables only -- this is always safe*)
    1.25  fun bound_hyp_subst_tac ctxt =
    1.26 @@ -306,7 +306,7 @@
    1.27      (Scan.succeed (fn ctxt => SIMPLE_METHOD'
    1.28          (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
    1.29      "substitution using an assumption, eliminating assumptions" #>
    1.30 -  hyp_subst_thins_setup #>
    1.31 +  hyp_subst_thin_setup #>
    1.32    Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
    1.33      "simple substitution";
    1.34