# HG changeset patch
# User wenzelm
# Date 1404487143 -7200
# Node ID cca0db87b653c8a125449976d214ec294a82700d
# Parent  19240ff4b02da302626086831df1b54fa64f2924
more uniform names;

diff -r 19240ff4b02d -r cca0db87b653 src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Fri Jul 04 16:50:57 2014 +0200
+++ b/src/Provers/hypsubst.ML	Fri Jul 04 17:19:03 2014 +0200
@@ -48,7 +48,7 @@
 sig
   val bound_hyp_subst_tac    : Proof.context -> int -> tactic
   val hyp_subst_tac_thin     : bool -> Proof.context -> int -> tactic
-  val hyp_subst_thins        : bool Config.T
+  val hyp_subst_thin         : bool Config.T
   val hyp_subst_tac          : Proof.context -> int -> tactic
   val blast_hyp_subst_tac    : bool -> int -> tactic
   val stac                   : thm -> int -> tactic
@@ -228,11 +228,11 @@
     gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
     if thin then thin_free_eq_tac else K no_tac];
 
-val (hyp_subst_thins, hyp_subst_thins_setup) = Attrib.config_bool
+val (hyp_subst_thin, hyp_subst_thin_setup) = Attrib.config_bool
     @{binding hypsubst_thin} (K false);
 
 fun hyp_subst_tac ctxt = hyp_subst_tac_thin
-    (Config.get ctxt hyp_subst_thins) ctxt
+    (Config.get ctxt hyp_subst_thin) ctxt
 
 (*Substitutes for Bound variables only -- this is always safe*)
 fun bound_hyp_subst_tac ctxt =
@@ -306,7 +306,7 @@
     (Scan.succeed (fn ctxt => SIMPLE_METHOD'
         (CHANGED_PROP o hyp_subst_tac_thin true ctxt)))
     "substitution using an assumption, eliminating assumptions" #>
-  hyp_subst_thins_setup #>
+  hyp_subst_thin_setup #>
   Method.setup @{binding simplesubst} (Attrib.thm >> (fn th => K (SIMPLE_METHOD' (stac th))))
     "simple substitution";