src/Tools/IsaPlanner/isand.ML
changeset 46777 1ce61ee1571a
parent 46217 7b19666f0e3d
child 49339 d1fcb4de8349
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Sat Mar 03 21:52:15 2012 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sat Mar 03 22:11:51 2012 +0100
     1.3 @@ -270,7 +270,7 @@
     1.4  
     1.5  (* make free vars into schematic vars with index zero *)
     1.6   fun unfix_frees frees = 
     1.7 -     apply (map (K (Thm.forall_elim_var 0)) frees) 
     1.8 +     fold (K (Thm.forall_elim_var 0)) frees
     1.9       o Drule.forall_intr_list frees;
    1.10  
    1.11  (* fix term and type variables *)