src/HOL/Tools/ATP/atp_util.ML
changeset 43864 58a7b3fdc193
parent 43863 a43d61270142
child 44392 6750b4297691
     1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:12:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:21:19 2011 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val s_disj : term * term -> term
     1.5    val s_imp : term * term -> term
     1.6    val s_iff : term * term -> term
     1.7 +  val close_form : term -> term
     1.8    val monomorphic_term : Type.tyenv -> term -> term
     1.9    val eta_expand : typ list -> term -> int -> term
    1.10    val transform_elim_prop : term -> term
    1.11 @@ -236,6 +237,11 @@
    1.12    | s_iff (t1, @{const True}) = t1
    1.13    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    1.14  
    1.15 +fun close_form t =
    1.16 +  fold (fn ((x, i), T) => fn t' =>
    1.17 +           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    1.18 +       (Term.add_vars t []) t
    1.19 +
    1.20  fun monomorphic_term subst =
    1.21    map_types (map_type_tvar (fn v =>
    1.22        case Type.lookup subst v of