src/Provers/simp.ML
 changeset 4271 3a82492e70c5 parent 3537 79ac9b475621 child 5961 6cf4e46ce95a
```     1.1 --- a/src/Provers/simp.ML	Fri Nov 21 15:27:43 1997 +0100
1.2 +++ b/src/Provers/simp.ML	Fri Nov 21 15:29:56 1997 +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(tac thm) of
1.8 +fun one_result(tac,thm) = case Seq.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  	  | Free _ => resolve_tac congs 1 ORELSE refl1_tac
1.14  	  | _ => refl1_tac))
1.15      val add_norm_tac = DEPTH_FIRST (has_fewer_prems nops) norm_step_tac
1.16 -    val Some(thm'',_) = Sequence.pull(add_norm_tac thm')
1.17 +    val Some(thm'',_) = Seq.pull(add_norm_tac thm')
1.18  in thm'' end;
1.19
1.21 @@ -443,7 +443,7 @@
1.22  fun simp_lhs(thm,ss,anet,ats,cs) =
1.23      if var_lhs(thm,i) then (ss,thm,anet,ats,cs) else
1.24      if lhs_is_NORM(thm,i) then (ss, res1(thm,trans_norms,i), anet,ats,cs)
1.25 -    else case Sequence.pull(cong_tac i thm) of
1.26 +    else case Seq.pull(cong_tac i thm) of
1.27  	    Some(thm',_) =>
1.28  		    let val ps = prems_of thm and ps' = prems_of thm';
1.29  			val n = length(ps')-length(ps);
1.30 @@ -467,7 +467,7 @@
1.31  	(ss,thm,anet',anet::ats,cs)
1.32      end;
1.33
1.34 -fun rew(seq,thm,ss,anet,ats,cs, more) = case Sequence.pull seq of
1.35 +fun rew(seq,thm,ss,anet,ats,cs, more) = case Seq.pull seq of
1.36        Some(thm',seq') =>
1.37  	    let val n = (nprems_of thm') - (nprems_of thm)
1.38  	    in pr_rew(i,n,thm,thm',more);
1.39 @@ -481,7 +481,7 @@
1.40  	    else (ss,thm,anet,ats,cs);
1.41
1.42  fun try_true(thm,ss,anet,ats,cs) =
1.43 -    case Sequence.pull(auto_tac i thm) of
1.44 +    case Seq.pull(auto_tac i thm) of
1.45        Some(thm',_) => (ss,thm',anet,ats,cs)
1.46      | None => let val (ss0,thm0,anet0,ats0,seq,more)::cs0 = cs
1.47  	      in if !tracing
1.48 @@ -492,7 +492,7 @@
1.49  	      end;
1.50
1.51  fun split(thm,ss,anet,ats,cs) =
1.52 -	case Sequence.pull(tapply(split_tac
1.53 +	case Seq.pull(tapply(split_tac
1.54                                    (cong_tac i,splits,split_consts) i,thm)) of
1.55  		Some(thm',_) => (SIMP_LHS::SPLIT::ss,thm',anet,ats,cs)
1.56  	      | None => (ss,thm,anet,ats,cs);
```