# HG changeset patch
# User wenzelm
# Date 1353171352 -3600
# Node ID 289181e3e524dcfdfa58265e9cca69c7ddb7cd3f
# Parent  e12e4ad9318380290129835dc08d7a3b071bbf30
tuned signature;

diff -r e12e4ad93183 -r 289181e3e524 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/HOL/Product_Type.thy	Sat Nov 17 17:55:52 2012 +0100
@@ -407,7 +407,6 @@
 
 ML {*
   (* replace parameters of product type by individual component parameters *)
-  val safe_full_simp_tac = generic_simp_tac true (true, false, false);
   local (* filtering with exists_paired_all is an essential optimization *)
     fun exists_paired_all (Const ("all", _) $ Abs (_, T, t)) =
           can HOLogic.dest_prodT T orelse exists_paired_all t
@@ -423,7 +422,7 @@
     val unsafe_split_all_tac = SUBGOAL (fn (t, i) =>
       if exists_paired_all t then full_simp_tac ss i else no_tac);
     fun split_all th =
-   if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th;
+      if exists_paired_all (Thm.prop_of th) then full_simplify ss th else th;
   end;
 *}
 
diff -r e12e4ad93183 -r 289181e3e524 src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/HOL/Tools/arith_data.ML	Sat Nov 17 17:55:52 2012 +0100
@@ -73,7 +73,7 @@
 
 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
 
-fun mk_minus t = 
+fun mk_minus t =
   let val T = Term.fastype_of t
   in Const (@{const_name Groups.uminus}, T --> T) $ t end;
 
@@ -112,11 +112,10 @@
 
 fun simp_all_tac rules =
   let val ss0 = HOL_ss addsimps rules
-      val safe_simp_tac = generic_simp_tac true (false, false, false)
   in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end;
 
 fun simplify_meta_eq rules =
   let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}
-  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
+  in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end;
 
 end;
diff -r e12e4ad93183 -r 289181e3e524 src/HOL/Word/WordBitwise.thy
--- a/src/HOL/Word/WordBitwise.thy	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/HOL/Word/WordBitwise.thy	Sat Nov 17 17:55:52 2012 +0100
@@ -597,10 +597,10 @@
     no_split_ss addsimps @{thms xor3_simps carry_simps if_bool_simps}
   ])
 
-val tac = let
+val tac =
+  let
     val (ss, sss) = expand_word_eq_sss;
-    val st = generic_simp_tac true (true, false, false);
-  in foldr1 (op THEN_ALL_NEW) ((CHANGED o st ss) :: map st sss) end;
+  in foldr1 (op THEN_ALL_NEW) ((CHANGED o safe_full_simp_tac ss) :: map safe_full_simp_tac sss) end;
 
 end
 
diff -r e12e4ad93183 -r 289181e3e524 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/Provers/clasimp.ML	Sat Nov 17 17:55:52 2012 +0100
@@ -44,9 +44,6 @@
 
 (* simp as classical wrapper *)
 
-(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
-val safe_asm_full_simp_tac = Simplifier.generic_simp_tac true (true, true, true);
-
 fun clasimp f name tac ctxt =
   Classical.map_claset (fn cs => f (cs, (name, CHANGED o tac (simpset_of ctxt)))) ctxt;
 
diff -r e12e4ad93183 -r 289181e3e524 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat Nov 17 17:42:19 2012 +0100
+++ b/src/Pure/simplifier.ML	Sat Nov 17 17:55:52 2012 +0100
@@ -13,13 +13,16 @@
   val global_simpset_of: theory -> simpset
   val Addsimprocs: simproc list -> unit
   val Delsimprocs: simproc list -> unit
-  val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
-  val safe_asm_full_simp_tac: simpset -> int -> tactic
   val simp_tac: simpset -> int -> tactic
   val asm_simp_tac: simpset -> int -> tactic
   val full_simp_tac: simpset -> int -> tactic
   val asm_lr_simp_tac: simpset -> int -> tactic
   val asm_full_simp_tac: simpset -> int -> tactic
+  val safe_simp_tac: simpset -> int -> tactic
+  val safe_asm_simp_tac: simpset -> int -> tactic
+  val safe_full_simp_tac: simpset -> int -> tactic
+  val safe_asm_lr_simp_tac: simpset -> int -> tactic
+  val safe_asm_full_simp_tac: simpset -> int -> tactic
   val simplify: simpset -> thm -> thm
   val asm_simplify: simpset -> thm -> thm
   val full_simplify: simpset -> thm -> thm
@@ -266,6 +269,12 @@
 val full_simp_tac = generic_simp_tac false (true, false, false);
 val asm_lr_simp_tac = generic_simp_tac false (true, true, false);
 val asm_full_simp_tac = generic_simp_tac false (true, true, true);
+
+(*not totally safe: may instantiate unknowns that appear also in other subgoals*)
+val safe_simp_tac = generic_simp_tac true (false, false, false);
+val safe_asm_simp_tac = generic_simp_tac true (false, true, false);
+val safe_full_simp_tac = generic_simp_tac true (true, false, false);
+val safe_asm_lr_simp_tac = generic_simp_tac true (true, true, false);
 val safe_asm_full_simp_tac = generic_simp_tac true (true, true, true);