src/Tools/IsaPlanner/isand.ML
changeset 52242 2d634bfa1bbf
parent 49340 25fc6e0da459
child 52244 cb15da7bd550
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu May 30 16:48:50 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu May 30 16:53:32 2013 +0200
     1.3 @@ -53,17 +53,15 @@
     1.4      let
     1.5        val premts = Thm.prems_of th;
     1.6  
     1.7 -      fun allify_prem_var (vt as (n,ty),t)  =
     1.8 +      fun allify_prem_var (vt as (n,ty)) t =
     1.9            (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    1.10  
    1.11 -      fun allify_prem Ts p = List.foldr allify_prem_var p Ts
    1.12 +      val allify_prem = fold_rev allify_prem_var
    1.13  
    1.14        val cTs = map (ctermify o Free) Ts
    1.15        val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.16        val allifyied_asm_thms = map (Drule.forall_elim_list cTs o Thm.assume) cterm_asms
    1.17 -    in
    1.18 -      (Library.foldl (fn (x,y) => y COMP x) (th, allifyied_asm_thms), cterm_asms)
    1.19 -    end;
    1.20 +    in (fold (curry op COMP) allifyied_asm_thms th, cterm_asms) end;
    1.21  
    1.22  (* make free vars into schematic vars with index zero *)
    1.23  fun unfix_frees frees =