src/Pure/unify.ML
changeset 23178 07ba6b58b3d2
parent 20664 ffbc5a57191a
child 24178 4ff1dc2aa18d
     1.1 --- a/src/Pure/unify.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/unify.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -280,7 +280,7 @@
     1.4    Clever would be to re-do just the affected dpairs*)
     1.5  fun SIMPL thy (env,dpairs) : Envir.env * dpair list * dpair list =
     1.6      let val all as (env',flexflex,flexrigid) =
     1.7 -      foldr (SIMPL0 thy) (env,[],[]) dpairs;
     1.8 +      List.foldr (SIMPL0 thy) (env,[],[]) dpairs;
     1.9    val dps = flexrigid@flexflex
    1.10      in if exists (fn ((_,t,u)) => changed(env',t) orelse changed(env',u)) dps
    1.11         then SIMPL thy (env',dps) else all
    1.12 @@ -471,7 +471,7 @@
    1.13    val (Ts,U) = strip_type env T
    1.14    and js = length ts - 1  downto 0
    1.15    val args = sort (make_ord arg_less)
    1.16 -    (foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
    1.17 +    (List.foldr (change_arg banned) [] (flexargs (js,ts,Ts)))
    1.18    val ts' = map (#t) args
    1.19      in
    1.20      if decreasing (length Ts) args then (env, (list_comb(Var(v,T), ts')))
    1.21 @@ -504,7 +504,7 @@
    1.22              then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
    1.23              else  (j::bnos, newbinder);   (*remove*)
    1.24        val indices = 0 upto (length rbinder - 1);
    1.25 -      val (banned,rbin') = foldr add_index ([],[]) (rbinder~~indices);
    1.26 +      val (banned,rbin') = List.foldr add_index ([],[]) (rbinder~~indices);
    1.27        val (env', t') = clean_term banned (env, t);
    1.28        val (env'',u') = clean_term banned (env',u)
    1.29    in  (ff_assign thy (env'', rbin', t', u'), tpairs)
    1.30 @@ -558,7 +558,7 @@
    1.31      then print_dpairs thy "Enter SIMPL" (env,dpairs)  else ();
    1.32      SIMPL thy (env,dpairs))
    1.33      in case flexrigid of
    1.34 -        [] => SOME (foldr (add_ffpair thy) (env',[]) flexflex, reseq)
    1.35 +        [] => SOME (List.foldr (add_ffpair thy) (env',[]) flexflex, reseq)
    1.36        | dp::frigid' =>
    1.37      if tdepth > !search_bound then
    1.38          (warning "Unification bound exceeded"; Seq.pull reseq)
    1.39 @@ -607,7 +607,7 @@
    1.40  
    1.41  (*Smash all flex-flexpairs.  Should allow selection of pairs by a predicate?*)
    1.42  fun smash_flexflex (env,tpairs) : Envir.env =
    1.43 -  foldr smash_flexflex1 env tpairs;
    1.44 +  List.foldr smash_flexflex1 env tpairs;
    1.45  
    1.46  (*Returns unifiers with no remaining disagreement pairs*)
    1.47  fun smash_unifiers thy tus env =