[isabelle-dev] Malformed YXML encoding

[Steve Wong]

Hi,

I'm trying to generate a proof goal from string using the following:

fun generate x lthy =
    let
        val thy = Local_Theory.exit_global lthy
        val ctxt = ProofContext.init_global thy
    in
        (Specification.theorem_cmd
             Thm.lemmaK NONE (K I)
             (Binding.name "", []) []

             (Element.Shows [(Attrib.empty_binding,
                              [(Syntax.string_of_term ctxt @{term "F"} ^ " =
" ^
                                Syntax.string_of_term ctxt @{term "G"}

, [])])]) x lthy)
    end


val _ =
    Outer_Syntax.local_theory_to_proof' "generate" Thm.lemmaK
Keyword.thy_goal
    (Scan.succeed generate)

Unfortunately I keep getting an error saying:

*** Malformed YXML encoding: multiple results
*** At command "verify_with"

But, if I change the generate function to

fun generate x lthy =
    let
        val thy = Local_Theory.exit_global lthy
        val ctxt = ProofContext.init_global thy
    in
        (Specification.theorem_cmd
             Thm.lemmaK NONE (K I)
             (Binding.name "", []) []

             (Element.Shows [(Attrib.empty_binding,
                              [((Syntax.string_of_term ctxt @{term "F = G"})

, [])])]) x lthy)
    end

then the proof goal is properly generated. Notice that in the second
version, the string is created from a single term on the string "F = G",
whereas the string in the first is created by concatenating together 3
individual strings: string of @{term "F"}, "=", and string of @{term "G"}.
How come there is a difference? This is just a toy example, because I'm
actually dealing with variable terms, so it's not as simple as "F" and "G".

Please help. Thanks.

Steve
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110826/80183243/attachment.html>