fixed Isabelle version of lightweight tag theorem, using "Thm.trivial" not "Thm.assume"

--- a/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -55,9 +55,10 @@
 fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th)
   | used_axioms _ _ = NONE
 
-fun cterm_from_metis ctxt sym_tab tm =
+fun cterm_from_metis ctxt sym_tab wrap tm =
   let val thy = Proof_Context.theory_of ctxt in
     tm |> hol_term_from_metis MX sym_tab ctxt
+       |> wrap
        |> Syntax.check_term
               (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
        |> cterm_of thy
@@ -70,10 +71,11 @@
 fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth =
   (case Metis_LiteralSet.toList (Metis_Thm.clause mth) of
      [(true, (_, [_, tm]))] =>
-     tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive
+     tm |> cterm_from_metis ctxt sym_tab I |> Thm.reflexive
      RS @{thm meta_eq_to_obj_eq}
    | [_, (_, tm)] =>
-     tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume
+     tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab HOLogic.mk_Trueprop
+        |> Thm.trivial
    | _ => raise Fail "unexpected tags sym clause")
   |> Meson.make_meta_clause