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.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)