src/HOL/Tools/Meson/meson_clausify.ML
changeset 60781 2da59cdf531c
parent 60642 48dd1cefb4ae
child 60801 7664e0916eec
     1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Sat Jul 25 23:15:37 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Sat Jul 25 23:41:53 2015 +0200
     1.3 @@ -94,10 +94,6 @@
     1.4    | is_quasi_lambda_free (Abs _) = false
     1.5    | is_quasi_lambda_free _ = true
     1.6  
     1.7 -val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
     1.8 -val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
     1.9 -val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
    1.10 -
    1.11  (* FIXME: Requires more use of cterm constructors. *)
    1.12  fun abstract ctxt ct =
    1.13    let
    1.14 @@ -118,7 +114,8 @@
    1.15                 if Term.is_dependent rand then (*S*)
    1.16                   let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
    1.17                       val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
    1.18 -                     val abs_S' = cterm_instantiate [(f_S,crator),(g_S,crand)] @{thm abs_S}
    1.19 +                     val abs_S' =
    1.20 +                      infer_instantiate ctxt [(("f", 0), crator), (("g", 0), crand)] @{thm abs_S}
    1.21                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_S')
    1.22                   in
    1.23                     Thm.transitive abs_S' (Conv.binop_conv (abstract ctxt) rhs)
    1.24 @@ -126,7 +123,8 @@
    1.25                 else (*C*)
    1.26                   let val crator = Thm.cterm_of ctxt (Abs (x, xT, rator))
    1.27                       val abs_C' =
    1.28 -                      cterm_instantiate [(f_C, crator), (g_C, Thm.cterm_of ctxt rand)] @{thm abs_C}
    1.29 +                      infer_instantiate ctxt [(("f", 0), crator), (("b", 0), Thm.cterm_of ctxt rand)]
    1.30 +                        @{thm abs_C}
    1.31                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_C')
    1.32                   in
    1.33                     Thm.transitive abs_C' (Conv.fun_conv (Conv.arg_conv (abstract ctxt)) rhs)
    1.34 @@ -136,7 +134,8 @@
    1.35                 else (*B*)
    1.36                   let val crand = Thm.cterm_of ctxt (Abs (x, xT, rand))
    1.37                       val crator = Thm.cterm_of ctxt rator
    1.38 -                     val abs_B' = cterm_instantiate [(f_B,crator),(g_B,crand)] @{thm abs_B}
    1.39 +                     val abs_B' =
    1.40 +                      infer_instantiate ctxt [(("a", 0), crator), (("g", 0), crand)] @{thm abs_B}
    1.41                       val (_,rhs) = Thm.dest_equals (Thm.cprop_of abs_B')
    1.42                   in Thm.transitive abs_B' (Conv.arg_conv (abstract ctxt) rhs) end
    1.43              else makeK ()