src/Tools/IsaPlanner/isand.ML
changeset 46217 7b19666f0e3d
parent 44121 44adaa6db327
child 46777 1ce61ee1571a
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 18:18:06 2012 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sat Jan 14 19:06:05 2012 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4        val premts = Thm.prems_of th;
     1.5      
     1.6        fun allify_prem_var (vt as (n,ty),t)  = 
     1.7 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
     1.8 +          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
     1.9  
    1.10        fun allify_prem Ts p = List.foldr allify_prem_var p Ts
    1.11  
    1.12 @@ -171,7 +171,7 @@
    1.13  fun assume_allified sgn (tyvs,vs) t = 
    1.14      let
    1.15        fun allify_var (vt as (n,ty),t)  = 
    1.16 -          (Term.all ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    1.17 +          (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (Free vt, t)))
    1.18        fun allify Ts p = List.foldr allify_var p Ts
    1.19  
    1.20        val ctermify = Thm.cterm_of sgn;
    1.21 @@ -303,7 +303,7 @@
    1.22  fun allify_term (v, t) = 
    1.23      let val vt = #t (Thm.rep_cterm v)
    1.24        val (n,ty) = Term.dest_Free vt
    1.25 -    in (Term.all ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
    1.26 +    in (Logic.all_const ty) $ (Abs(n,ty,Term.abstract_over (vt, t))) end;
    1.27  
    1.28  fun allify_for_sg_term ctermify vs t =
    1.29      let val t_alls = List.foldr allify_term t vs;