src/FOL/simpdata.ML
changeset 4477 b3e5857d8d99
parent 4349 50403e5a44c0
child 4649 89ad3eb863a1
     1.1 --- a/src/FOL/simpdata.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -362,14 +362,25 @@
     1.4  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
     1.5  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
     1.6  
     1.7 -fun auto_tac (cs,ss) = 
     1.8 +
     1.9 +fun mk_auto_tac (cs, ss) m n =
    1.10      let val cs' = cs addss ss 
    1.11 -    in  EVERY [TRY (safe_tac cs'),
    1.12 -	       REPEAT (FIRSTGOAL (fast_tac cs')),
    1.13 +	val bdt = Blast.depth_tac cs m;
    1.14 +	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
    1.15 +		(warning ("Blast_tac: " ^ s); Seq.empty);
    1.16 +        val maintac = 
    1.17 +          blast_depth_tac	   (*fast but can't use addss*)
    1.18 +          ORELSE'
    1.19 +          depth_tac cs' n;         (*slower but general*)
    1.20 +    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
    1.21 +	       TRY (safe_tac cs'),
    1.22 +	       REPEAT (FIRSTGOAL maintac),
    1.23                 TRY (safe_tac (cs addSss ss)),
    1.24  	       prune_params_tac] 
    1.25      end;
    1.26  
    1.27 -fun Auto_tac () = auto_tac (claset(), simpset());
    1.28 +fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
    1.29  
    1.30 -fun auto () = by (Auto_tac ());
    1.31 +fun Auto_tac st = auto_tac (claset(), simpset()) st;
    1.32 +
    1.33 +fun auto () = by Auto_tac;