src/HOL/simpdata.ML
changeset 4651 70dd492a1698
parent 4640 ac6cf9f18653
child 4652 d24cca140eeb
     1.1 --- a/src/HOL/simpdata.ML	Wed Feb 25 15:48:04 1998 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Wed Feb 25 15:51:24 1998 +0100
     1.3 @@ -447,8 +447,9 @@
     1.4  
     1.5  (*Add a simpset to a classical set!*)
     1.6  infix 4 addSss addss;
     1.7 -fun cs addSss ss = cs addSaltern (CHANGED o (safe_asm_more_full_simp_tac ss));
     1.8 -fun cs addss  ss = cs addbefore                        asm_full_simp_tac ss;
     1.9 +fun cs addSss ss = cs addSaltern ("safe_asm_more_full_simp_tac",
    1.10 +				  CHANGED o (safe_asm_more_full_simp_tac ss));
    1.11 +fun cs addss  ss = cs addbefore  ("asm_full_simp_tac", asm_full_simp_tac ss);
    1.12  
    1.13  fun Addss ss = (claset_ref() := claset() addss ss);
    1.14  
    1.15 @@ -485,7 +486,7 @@
    1.16  	   with dup_step_tac when they are combined by auto_tac *)
    1.17  	fun nodup_depth_tac cs m i state = 
    1.18  	  SELECT_GOAL 
    1.19 -	   (getWrapper cs
    1.20 +	   (appWrappers cs
    1.21  	    (fn i => REPEAT_DETERM1 (COND (has_fewer_prems i) no_tac
    1.22  				     (safe_step_tac cs i)) THEN_ELSE
    1.23  	     (DEPTH_SOLVE (nodup_depth_tac cs m i),