1.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 19 21:37:12 2012 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Jan 19 21:37:12 2012 +0100
     1.3 @@ -140,7 +140,7 @@
     1.4        val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
     1.5        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
     1.6        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)
     1.7 -      val type_enc = type_enc_from_string Sound type_enc
     1.8 +      val type_enc = type_enc_from_string Strict type_enc
     1.9        val (sym_tab, axioms, concealed) =
    1.10          prepare_metis_problem ctxt type_enc lam_trans cls ths
    1.11        fun get_isa_thm mth Isa_Reflexive_or_Trivial =