src/HOL/Tools/Metis/metis_generate.ML
changeset 60358 aebfbcab1eb8
parent 59877 a04ea4709c8d
child 61860 2ce3d12015b3
     1.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 02 09:10:05 2015 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 02 09:16:19 2015 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  
     1.5  val proxy_defs = map (fst o snd o snd) proxy_table
     1.6  fun prepare_helper ctxt =
     1.7 -  Meson.make_meta_clause #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
     1.8 +  Meson.make_meta_clause ctxt #> rewrite_rule ctxt (map safe_mk_meta_eq proxy_defs)
     1.9  
    1.10  fun metis_term_of_atp type_enc (ATerm ((s, []), tms)) =
    1.11    if is_tptp_variable s then
    1.12 @@ -181,7 +181,7 @@
    1.13            SOME s =>
    1.14            let val s = s |> space_explode "_" |> tl |> space_implode "_" in
    1.15              (case Int.fromString s of
    1.16 -              SOME j => Meson.make_meta_clause (snd (nth clauses j)) |> Isa_Raw |> some
    1.17 +              SOME j => Meson.make_meta_clause ctxt (snd (nth clauses j)) |> Isa_Raw |> some
    1.18              | NONE =>
    1.19                if String.isPrefix lam_fact_prefix (unascii_of s) then Isa_Lambda_Lifted |> some
    1.20                else raise Fail ("malformed fact identifier " ^ quote ident))