src/Tools/IsaPlanner/rw_inst.ML
changeset 30190 479806475f3c
parent 29270 0eade173f77e
child 33037 b22e44496dc2
--- a/src/Tools/IsaPlanner/rw_inst.ML	Sun Mar 01 16:48:06 2009 +0100
+++ b/src/Tools/IsaPlanner/rw_inst.ML	Sun Mar 01 23:36:12 2009 +0100
@@ -136,7 +136,7 @@
 fun mk_renamings tgt rule_inst = 
     let
       val rule_conds = Thm.prems_of rule_inst
-      val names = foldr OldTerm.add_term_names [] (tgt :: rule_conds);
+      val names = List.foldr OldTerm.add_term_names [] (tgt :: rule_conds);
       val (conds_tyvs,cond_vs) = 
           Library.foldl (fn ((tyvs, vs), t) => 
                     (Library.union
@@ -147,7 +147,7 @@
       val termvars = map Term.dest_Var (OldTerm.term_vars tgt); 
       val vars_to_fix = Library.union (termvars, cond_vs);
       val (renamings, names2) = 
-          foldr (fn (((n,i),ty), (vs, names')) => 
+          List.foldr (fn (((n,i),ty), (vs, names')) => 
                     let val n' = Name.variant names' n in
                       ((((n,i),ty), Free (n', ty)) :: vs, n'::names')
                     end)
@@ -166,13 +166,13 @@
     let 
       val ignore_ixs = map fst ignore_insts;
       val (tvars, tfrees) = 
-            foldr (fn (t, (varixs, tfrees)) => 
+            List.foldr (fn (t, (varixs, tfrees)) => 
                       (OldTerm.add_term_tvars (t,varixs),
                        OldTerm.add_term_tfrees (t,tfrees)))
                   ([],[]) ts;
         val unfixed_tvars = 
             List.filter (fn (ix,s) => not (member (op =) ignore_ixs ix)) tvars;
-        val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars
+        val (fixtyinsts, _) = List.foldr new_tfree ([], map fst tfrees) unfixed_tvars
     in (fixtyinsts, tfrees) end;
 
 
@@ -248,7 +248,7 @@
                           Ts;
 
       (* type-instantiate the var instantiations *)
-      val insts_tyinst = foldr (fn ((ix,(ty,t)),insts_tyinst) => 
+      val insts_tyinst = List.foldr (fn ((ix,(ty,t)),insts_tyinst) => 
                             (ix, (Term.typ_subst_TVars term_typ_inst ty, 
                                   Term.subst_TVars term_typ_inst t))
                             :: insts_tyinst)