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.20  fun add_norm_tags congs =
    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);