src/Tools/IsaPlanner/isand.ML
changeset 30190 479806475f3c
parent 29270 0eade173f77e
child 31945 d5f186aa0bed
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4        fun allify_prem_var (vt as (n,ty),t)  = 
     1.5            (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
     1.6  
     1.7 -      fun allify_prem Ts p = foldr allify_prem_var p Ts
     1.8 +      fun allify_prem Ts p = List.foldr allify_prem_var p Ts
     1.9  
    1.10        val cTs = map (ctermify o Free) Ts
    1.11        val cterm_asms = map (ctermify o allify_prem Ts) premts
    1.12 @@ -306,7 +306,7 @@
    1.13      in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
    1.14  
    1.15  fun allify_for_sg_term ctermify vs t =
    1.16 -    let val t_alls = foldr allify_term t vs;
    1.17 +    let val t_alls = List.foldr allify_term t vs;
    1.18          val ct_alls = ctermify t_alls; 
    1.19      in 
    1.20        (ct_alls, Drule.forall_elim_list vs (Thm.assume ct_alls))
    1.21 @@ -394,7 +394,7 @@
    1.22                  |> Drule.forall_intr_list cfvs
    1.23      in Drule.compose_single (solth', i, gth) end;
    1.24  
    1.25 -fun export_solutions (xs,th) = foldr (uncurry export_solution) th xs;
    1.26 +fun export_solutions (xs,th) = List.foldr (uncurry export_solution) th xs;
    1.27  
    1.28  
    1.29  (* fix parameters of a subgoal "i", as free variables, and create an