src/Provers/simp.ML
changeset 1512 ce37c64244c0
parent 611 11098f505bfe
child 2266 82aef6857c5b
     1.1 --- a/src/Provers/simp.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Provers/simp.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -129,7 +129,7 @@
     1.4  in mk trans_thms end;
     1.5  
     1.6  (*Applies tactic and returns the first resulting state, FAILS if none!*)
     1.7 -fun one_result(tac,thm) = case Sequence.pull(tapply(tac,thm)) of
     1.8 +fun one_result(tac,thm) = case Sequence.pull(tac thm) of
     1.9  	Some(thm',_) => thm'
    1.10        | None => raise THM("Simplifier: could not continue", 0, [thm]);
    1.11  
    1.12 @@ -205,7 +205,7 @@
    1.13  			     resolve_tac congs 1 ORELSE refl1_tac
    1.14  		| Free _ => resolve_tac congs 1 ORELSE refl1_tac
    1.15  		| _ => refl1_tac))
    1.16 -    val Some(thm'',_) = Sequence.pull(tapply(add_norm_tac,thm'))
    1.17 +    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
    1.18  in thm'' end;
    1.19  
    1.20  fun add_norm_tags congs =
    1.21 @@ -357,18 +357,18 @@
    1.22  fun split_tac (cong_tac,splits,split_consts) i =
    1.23      let fun seq_try (split::splits,a::bs) thm = tapply(
    1.24  		COND (splittable a i) (DETERM(resolve_tac[split]i))
    1.25 -			(Tactic(seq_try(splits,bs))), thm)
    1.26 -	      | seq_try([],_) thm = tapply(no_tac,thm)
    1.27 -	and try_rew thm = tapply(Tactic(seq_try(splits,split_consts))
    1.28 -				 ORELSE Tactic one_subt, thm)
    1.29 +			((seq_try(splits,bs))), thm)
    1.30 +	      | seq_try([],_) thm = no_tac thm
    1.31 +	and try_rew thm = tapply((seq_try(splits,split_consts))
    1.32 +				 ORELSE one_subt, thm)
    1.33  	and one_subt thm =
    1.34  		let val test = has_fewer_prems (nprems_of thm + 1)
    1.35  		    fun loop thm = tapply(COND test no_tac
    1.36 -			((Tactic try_rew THEN DEPTH_FIRST test (refl_tac i))
    1.37 -			 ORELSE (refl_tac i THEN Tactic loop)), thm)
    1.38 -		in tapply(cong_tac THEN Tactic loop, thm) end
    1.39 +			((try_rew THEN DEPTH_FIRST test (refl_tac i))
    1.40 +			 ORELSE (refl_tac i THEN loop)), thm)
    1.41 +		in (cong_tac THEN loop) thm end
    1.42      in if null splits then no_tac
    1.43 -       else COND (may_match(split_consts,i)) (Tactic try_rew) no_tac
    1.44 +       else COND (may_match(split_consts,i)) try_rew no_tac
    1.45      end;
    1.46  
    1.47  fun SPLIT_TAC (SS{cong_net,splits,split_consts,...}) i =
    1.48 @@ -443,7 +443,7 @@
    1.49  fun simp_lhs(thm,ss,anet,ats,cs) =
    1.50      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
    1.51      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
    1.52 -    else case Sequence.pull(tapply(cong_tac i,thm)) of
    1.53 +    else case Sequence.pull(cong_tac i thm) of
    1.54  	    Some(thm',_) =>
    1.55  		    let val ps = prems_of thm and ps' = prems_of thm';
    1.56  			val n = length(ps')-length(ps);
    1.57 @@ -481,7 +481,7 @@
    1.58  	    else (ss,thm,anet,ats,cs);
    1.59  
    1.60  fun try_true(thm,ss,anet,ats,cs) =
    1.61 -    case Sequence.pull(tapply(auto_tac i,thm)) of
    1.62 +    case Sequence.pull(auto_tac i thm) of
    1.63        Some(thm',_) => (ss,thm',anet,ats,cs)
    1.64      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
    1.65  	      in if !tracing
    1.66 @@ -501,7 +501,7 @@
    1.67  	  MK_EQ => (ss, res1(thm,[red2],i), anet, ats, cs)
    1.68  	| ASMS(a) => add_asms(ss,thm,a,anet,ats,cs)
    1.69  	| SIMP_LHS => simp_lhs(thm,ss,anet,ats,cs)
    1.70 -	| REW => rew(tapply(net_tac net i,thm),thm,ss,anet,ats,cs,true)
    1.71 +	| REW => rew(net_tac net i thm,thm,ss,anet,ats,cs,true)
    1.72  	| REFL => (ss, res1(thm,refl_thms,i), anet, ats, cs)
    1.73  	| TRUE => try_true(res1(thm,refl_thms,i),ss,anet,ats,cs)
    1.74  	| PROVE => (if if_fl then MK_EQ::SIMP_LHS::SPLIT::TRUE::ss