added "trace_metis" configuration option, replacing old-fashioned references
authorblanchet
Mon Oct 11 18:02:14 2010 +0700 (2010-10-11)
changeset 3997811bfb7e7cc86
parent 39977 c9cbc16e93ce
child 39979 b13515940b53
added "trace_metis" configuration option, replacing old-fashioned references
src/HOL/Tools/Metis/metis_reconstruct.ML
src/HOL/Tools/Metis/metis_tactics.ML
     1.1 --- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Sun Oct 10 23:16:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Mon Oct 11 18:02:14 2010 +0700
     1.3 @@ -11,7 +11,8 @@
     1.4  sig
     1.5    type mode = Metis_Translate.mode
     1.6  
     1.7 -  val trace : bool Unsynchronized.ref
     1.8 +  val trace : bool Config.T
     1.9 +  val trace_msg : Proof.context -> (unit -> string) -> unit
    1.10    val lookth : (Metis_Thm.thm * 'a) list -> Metis_Thm.thm -> 'a
    1.11    val untyped_aconv : term -> term -> bool
    1.12    val replay_one_inference :
    1.13 @@ -20,6 +21,7 @@
    1.14      -> (Metis_Thm.thm * thm) list
    1.15    val discharge_skolem_premises :
    1.16      Proof.context -> (thm * term) option list -> thm -> thm
    1.17 +  val setup : theory -> theory
    1.18  end;
    1.19  
    1.20  structure Metis_Reconstruct : METIS_RECONSTRUCT =
    1.21 @@ -27,8 +29,9 @@
    1.22  
    1.23  open Metis_Translate
    1.24  
    1.25 -val trace = Unsynchronized.ref false
    1.26 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
    1.27 +val (trace, trace_setup) = Attrib.config_bool "trace_metis" (K false)
    1.28 +
    1.29 +fun trace_msg ctxt msg = if Config.get ctxt trace then tracing (msg ()) else ()
    1.30  
    1.31  datatype term_or_type = SomeTerm of term | SomeType of typ
    1.32  
    1.33 @@ -92,8 +95,8 @@
    1.34  (*Maps metis terms to isabelle terms*)
    1.35  fun hol_term_from_metis_PT ctxt fol_tm =
    1.36    let val thy = ProofContext.theory_of ctxt
    1.37 -      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
    1.38 -                                  Metis_Term.toString fol_tm)
    1.39 +      val _ = trace_msg ctxt (fn () => "hol_term_from_metis_PT: " ^
    1.40 +                                       Metis_Term.toString fol_tm)
    1.41        fun tm_to_tt (Metis_Term.Var v) =
    1.42               (case strip_prefix_and_unascii tvar_prefix v of
    1.43                    SOME w => SomeType (make_tvar w)
    1.44 @@ -160,8 +163,8 @@
    1.45  
    1.46  (*Maps fully-typed metis terms to isabelle terms*)
    1.47  fun hol_term_from_metis_FT ctxt fol_tm =
    1.48 -  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
    1.49 -                                  Metis_Term.toString fol_tm)
    1.50 +  let val _ = trace_msg ctxt (fn () => "hol_term_from_metis_FT: " ^
    1.51 +                                       Metis_Term.toString fol_tm)
    1.52        fun cvt (Metis_Term.Fn ("ti", [Metis_Term.Var v, _])) =
    1.53               (case strip_prefix_and_unascii schematic_var_prefix v of
    1.54                    SOME w =>  mk_var(w, dummyT)
    1.55 @@ -188,10 +191,12 @@
    1.56                | NONE => (*Not a constant. Is it a fixed variable??*)
    1.57              case strip_prefix_and_unascii fixed_var_prefix x of
    1.58                  SOME v => Free (v, dummyT)
    1.59 -              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
    1.60 -                  hol_term_from_metis_PT ctxt t))
    1.61 -        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    1.62 -            hol_term_from_metis_PT ctxt t)
    1.63 +              | NONE => (trace_msg ctxt (fn () =>
    1.64 +                                      "hol_term_from_metis_FT bad const: " ^ x);
    1.65 +                         hol_term_from_metis_PT ctxt t))
    1.66 +        | cvt t = (trace_msg ctxt (fn () =>
    1.67 +                   "hol_term_from_metis_FT bad term: " ^ Metis_Term.toString t);
    1.68 +                   hol_term_from_metis_PT ctxt t)
    1.69    in fol_tm |> cvt end
    1.70  
    1.71  fun hol_term_from_metis FT = hol_term_from_metis_FT
    1.72 @@ -199,11 +204,12 @@
    1.73  
    1.74  fun hol_terms_from_fol ctxt mode old_skolems fol_tms =
    1.75    let val ts = map (hol_term_from_metis mode ctxt) fol_tms
    1.76 -      val _ = trace_msg (fn () => "  calling type inference:")
    1.77 -      val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
    1.78 +      val _ = trace_msg ctxt (fn () => "  calling type inference:")
    1.79 +      val _ = app (fn t => trace_msg ctxt
    1.80 +                                     (fn () => Syntax.string_of_term ctxt t)) ts
    1.81        val ts' = ts |> map (reveal_old_skolem_terms old_skolems)
    1.82                     |> infer_types ctxt
    1.83 -      val _ = app (fn t => trace_msg
    1.84 +      val _ = app (fn t => trace_msg ctxt
    1.85                      (fn () => "  final term: " ^ Syntax.string_of_term ctxt t ^
    1.86                                "  of type  " ^ Syntax.string_of_typ ctxt (type_of t)))
    1.87                    ts'
    1.88 @@ -215,10 +221,10 @@
    1.89  
    1.90  (*for debugging only*)
    1.91  (*
    1.92 -fun print_thpair (fth,th) =
    1.93 -  (trace_msg (fn () => "=============================================");
    1.94 -   trace_msg (fn () => "Metis: " ^ Metis_Thm.toString fth);
    1.95 -   trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
    1.96 +fun print_thpair ctxt (fth,th) =
    1.97 +  (trace_msg ctxt (fn () => "=============================================");
    1.98 +   trace_msg ctxt (fn () => "Metis: " ^ Metis_Thm.toString fth);
    1.99 +   trace_msg ctxt (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   1.100  *)
   1.101  
   1.102  fun lookth thpairs (fth : Metis_Thm.thm) =
   1.103 @@ -264,12 +270,12 @@
   1.104              val t = hol_term_from_metis mode ctxt y
   1.105          in  SOME (cterm_of thy (Var v), t)  end
   1.106          handle Option.Option =>
   1.107 -               (trace_msg (fn () => "\"find_var\" failed for " ^ x ^
   1.108 -                                    " in " ^ Display.string_of_thm ctxt i_th);
   1.109 +               (trace_msg ctxt (fn () => "\"find_var\" failed for " ^ x ^
   1.110 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   1.111                  NONE)
   1.112               | TYPE _ =>
   1.113 -               (trace_msg (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   1.114 -                                    " in " ^ Display.string_of_thm ctxt i_th);
   1.115 +               (trace_msg ctxt (fn () => "\"hol_term_from_metis\" failed for " ^ x ^
   1.116 +                                         " in " ^ Display.string_of_thm ctxt i_th);
   1.117                  NONE)
   1.118        fun remove_typeinst (a, t) =
   1.119              case strip_prefix_and_unascii schematic_var_prefix a of
   1.120 @@ -277,14 +283,14 @@
   1.121                | NONE => case strip_prefix_and_unascii tvar_prefix a of
   1.122                  SOME _ => NONE          (*type instantiations are forbidden!*)
   1.123                | NONE => SOME (a,t)    (*internal Metis var?*)
   1.124 -      val _ = trace_msg (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   1.125 +      val _ = trace_msg ctxt (fn () => "  isa th: " ^ Display.string_of_thm ctxt i_th)
   1.126        val substs = map_filter remove_typeinst (Metis_Subst.toList fsubst)
   1.127        val (vars,rawtms) = ListPair.unzip (map_filter subst_translation substs)
   1.128        val tms = rawtms |> map (reveal_old_skolem_terms old_skolems)
   1.129                         |> infer_types ctxt
   1.130        val ctm_of = cterm_incr_types thy (1 + Thm.maxidx_of i_th)
   1.131        val substs' = ListPair.zip (vars, map ctm_of tms)
   1.132 -      val _ = trace_msg (fn () =>
   1.133 +      val _ = trace_msg ctxt (fn () =>
   1.134          cat_lines ("subst_translations:" ::
   1.135            (substs' |> map (fn (x, y) =>
   1.136              Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
   1.137 @@ -375,8 +381,8 @@
   1.138    let
   1.139      val thy = ProofContext.theory_of ctxt
   1.140      val i_th1 = lookth thpairs th1 and i_th2 = lookth thpairs th2
   1.141 -    val _ = trace_msg (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.142 -    val _ = trace_msg (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.143 +    val _ = trace_msg ctxt (fn () => "  isa th1 (pos): " ^ Display.string_of_thm ctxt i_th1)
   1.144 +    val _ = trace_msg ctxt (fn () => "  isa th2 (neg): " ^ Display.string_of_thm ctxt i_th2)
   1.145    in
   1.146      (* Trivial cases where one operand is type info *)
   1.147      if Thm.eq_thm (TrueI, i_th1) then
   1.148 @@ -387,15 +393,15 @@
   1.149        let
   1.150          val i_atm = singleton (hol_terms_from_fol ctxt mode old_skolems)
   1.151                                (Metis_Term.Fn atm)
   1.152 -        val _ = trace_msg (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.153 +        val _ = trace_msg ctxt (fn () => "  atom: " ^ Syntax.string_of_term ctxt i_atm)
   1.154          val prems_th1 = prems_of i_th1
   1.155          val prems_th2 = prems_of i_th2
   1.156          val index_th1 = literal_index (mk_not i_atm) prems_th1
   1.157                handle Empty => raise Fail "Failed to find literal in th1"
   1.158 -        val _ = trace_msg (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.159 +        val _ = trace_msg ctxt (fn () => "  index_th1: " ^ Int.toString index_th1)
   1.160          val index_th2 = literal_index i_atm prems_th2
   1.161                handle Empty => raise Fail "Failed to find literal in th2"
   1.162 -        val _ = trace_msg (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.163 +        val _ = trace_msg ctxt (fn () => "  index_th2: " ^ Int.toString index_th2)
   1.164      in
   1.165        resolve_inc_tyvars thy (select_literal index_th1 i_th1) index_th2 i_th2
   1.166      end
   1.167 @@ -411,7 +417,7 @@
   1.168  fun refl_inf ctxt mode old_skolems t =
   1.169    let val thy = ProofContext.theory_of ctxt
   1.170        val i_t = singleton (hol_terms_from_fol ctxt mode old_skolems) t
   1.171 -      val _ = trace_msg (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.172 +      val _ = trace_msg ctxt (fn () => "  term: " ^ Syntax.string_of_term ctxt i_t)
   1.173        val c_t = cterm_incr_types thy refl_idx i_t
   1.174    in  cterm_instantiate [(refl_x, c_t)] REFL_THM  end;
   1.175  
   1.176 @@ -430,7 +436,7 @@
   1.177    let val thy = ProofContext.theory_of ctxt
   1.178        val m_tm = Metis_Term.Fn atm
   1.179        val [i_atm,i_tm] = hol_terms_from_fol ctxt mode old_skolems [m_tm, fr]
   1.180 -      val _ = trace_msg (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.181 +      val _ = trace_msg ctxt (fn () => "sign of the literal: " ^ Bool.toString pos)
   1.182        fun replace_item_list lx 0 (_::ls) = lx::ls
   1.183          | replace_item_list lx i (l::ls) = l :: replace_item_list lx (i-1) ls
   1.184        fun path_finder_FO tm [] = (tm, Bound 0)
   1.185 @@ -444,7 +450,7 @@
   1.186                                  "equality_inf: " ^ Int.toString p ^ " adj " ^
   1.187                                  Int.toString adjustment ^ " term " ^
   1.188                                  Syntax.string_of_term ctxt tm)
   1.189 -                val _ = trace_msg (fn () => "path_finder: " ^ Int.toString p ^
   1.190 +                val _ = trace_msg ctxt (fn () => "path_finder: " ^ Int.toString p ^
   1.191                                        "  " ^ Syntax.string_of_term ctxt tm_p)
   1.192                  val (r,t) = path_finder_FO tm_p ps
   1.193              in
   1.194 @@ -496,12 +502,12 @@
   1.195          | path_finder_lit tm_a idx = path_finder mode tm_a idx m_tm
   1.196        val (tm_subst, body) = path_finder_lit i_atm fp
   1.197        val tm_abs = Abs ("x", type_of tm_subst, body)
   1.198 -      val _ = trace_msg (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.199 -      val _ = trace_msg (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.200 -      val _ = trace_msg (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.201 +      val _ = trace_msg ctxt (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
   1.202 +      val _ = trace_msg ctxt (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
   1.203 +      val _ = trace_msg ctxt (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
   1.204        val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst)  (*ill typed but gives right max*)
   1.205        val subst' = Thm.incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
   1.206 -      val _ = trace_msg (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.207 +      val _ = trace_msg ctxt (fn () => "subst' " ^ Display.string_of_thm ctxt subst')
   1.208        val eq_terms = map (pairself (cterm_of thy))
   1.209          (ListPair.zip (OldTerm.term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
   1.210    in  cterm_instantiate eq_terms subst'  end;
   1.211 @@ -540,13 +546,13 @@
   1.212  
   1.213  fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   1.214    let
   1.215 -    val _ = trace_msg (fn () => "=============================================")
   1.216 -    val _ = trace_msg (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   1.217 -    val _ = trace_msg (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   1.218 +    val _ = trace_msg ctxt (fn () => "=============================================")
   1.219 +    val _ = trace_msg ctxt (fn () => "METIS THM: " ^ Metis_Thm.toString fol_th)
   1.220 +    val _ = trace_msg ctxt (fn () => "INFERENCE: " ^ Metis_Proof.inferenceToString inf)
   1.221      val th = step ctxt mode old_skolems thpairs (fol_th, inf)
   1.222               |> flexflex_first_order
   1.223 -    val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.224 -    val _ = trace_msg (fn () => "=============================================")
   1.225 +    val _ = trace_msg ctxt (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
   1.226 +    val _ = trace_msg ctxt (fn () => "=============================================")
   1.227      val num_metis_lits =
   1.228        fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
   1.229               |> count is_metis_literal_genuine
   1.230 @@ -556,8 +562,6 @@
   1.231              else error "Cannot replay Metis proof in Isabelle: Out of sync."
   1.232    in (fol_th, th) :: thpairs end
   1.233  
   1.234 -(* FIXME ### GET RID OF skolem WRAPPER by looking at substitution *)
   1.235 -
   1.236  fun term_instantiate thy = cterm_instantiate o map (pairself (cterm_of thy))
   1.237  
   1.238  (* In principle, it should be sufficient to apply "assume_tac" to unify the
   1.239 @@ -790,8 +794,10 @@
   1.240                THEN ALLGOALS (fn i =>
   1.241                         rtac @{thm Meson.skolem_COMBK_I} i
   1.242                         THEN rotate_tac (rotation_for_subgoal i) i
   1.243 -                       THEN PRIMITIVE (unify_first_prem_with_concl thy i)
   1.244 +(*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
   1.245                         THEN assume_tac i)))
   1.246      end
   1.247  
   1.248 +val setup = trace_setup
   1.249 +
   1.250  end;
     2.1 --- a/src/HOL/Tools/Metis/metis_tactics.ML	Sun Oct 10 23:16:24 2010 +0200
     2.2 +++ b/src/HOL/Tools/Metis/metis_tactics.ML	Mon Oct 11 18:02:14 2010 +0700
     2.3 @@ -9,7 +9,6 @@
     2.4  
     2.5  signature METIS_TACTICS =
     2.6  sig
     2.7 -  val trace : bool Unsynchronized.ref
     2.8    val type_lits : bool Config.T
     2.9    val new_skolemizer : bool Config.T
    2.10    val metis_tac : Proof.context -> thm list -> int -> tactic
    2.11 @@ -24,8 +23,6 @@
    2.12  open Metis_Translate
    2.13  open Metis_Reconstruct
    2.14  
    2.15 -fun trace_msg msg = if !trace then tracing (msg ()) else ()
    2.16 -
    2.17  val (type_lits, type_lits_setup) = Attrib.config_bool "metis_type_lits" (K true)
    2.18  val (new_skolemizer, new_skolemizer_setup) =
    2.19    Attrib.config_bool "metis_new_skolemizer" (K false)
    2.20 @@ -67,21 +64,21 @@
    2.21               (0 upto length ths0 - 1) ths0
    2.22        val thss = map (snd o snd) th_cls_pairs
    2.23        val dischargers = map (fst o snd) th_cls_pairs
    2.24 -      val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    2.25 -      val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
    2.26 -      val _ = trace_msg (fn () => "THEOREM CLAUSES")
    2.27 -      val _ = app (app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th))) thss
    2.28 +      val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    2.29 +      val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    2.30 +      val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES")
    2.31 +      val _ = app (app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th))) thss
    2.32        val (mode, {axioms, tfrees, old_skolems}) =
    2.33          build_logic_map mode ctxt type_lits cls thss
    2.34        val _ = if null tfrees then ()
    2.35 -              else (trace_msg (fn () => "TFREE CLAUSES");
    2.36 +              else (trace_msg ctxt (fn () => "TFREE CLAUSES");
    2.37                      app (fn TyLitFree ((s, _), (s', _)) =>
    2.38 -                            trace_msg (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
    2.39 -      val _ = trace_msg (fn () => "CLAUSES GIVEN TO METIS")
    2.40 +                            trace_msg ctxt (fn () => s ^ "(" ^ s' ^ ")")) tfrees)
    2.41 +      val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS")
    2.42        val thms = map #1 axioms
    2.43 -      val _ = app (fn th => trace_msg (fn () => Metis_Thm.toString th)) thms
    2.44 -      val _ = trace_msg (fn () => "mode = " ^ string_of_mode mode)
    2.45 -      val _ = trace_msg (fn () => "START METIS PROVE PROCESS")
    2.46 +      val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms
    2.47 +      val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode)
    2.48 +      val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS")
    2.49    in
    2.50        case filter (is_false o prop_of) cls of
    2.51            false_th::_ => [false_th RS @{thm FalseE}]
    2.52 @@ -89,7 +86,7 @@
    2.53        case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []}
    2.54             |> Metis_Resolution.loop of
    2.55            Metis_Resolution.Contradiction mth =>
    2.56 -            let val _ = trace_msg (fn () => "METIS RECONSTRUCTION START: " ^
    2.57 +            let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^
    2.58                            Metis_Thm.toString mth)
    2.59                  val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt
    2.60                               (*add constraints arising from converting goal to clause form*)
    2.61 @@ -97,8 +94,8 @@
    2.62                  val result =
    2.63                    fold (replay_one_inference ctxt' mode old_skolems) proof axioms
    2.64                  and used = map_filter (used_axioms axioms) proof
    2.65 -                val _ = trace_msg (fn () => "METIS COMPLETED...clauses actually used:")
    2.66 -                val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) used
    2.67 +                val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:")
    2.68 +                val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used
    2.69                  val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) =>
    2.70                    if have_common_thm used cls then NONE else SOME name)
    2.71              in
    2.72 @@ -113,12 +110,12 @@
    2.73                    ();
    2.74                  case result of
    2.75                      (_,ith)::_ =>
    2.76 -                        (trace_msg (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    2.77 +                        (trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith);
    2.78                           [discharge_skolem_premises ctxt dischargers ith])
    2.79 -                  | _ => (trace_msg (fn () => "Metis: No result"); [])
    2.80 +                  | _ => (trace_msg ctxt (fn () => "Metis: No result"); [])
    2.81              end
    2.82          | Metis_Resolution.Satisfiable _ =>
    2.83 -            (trace_msg (fn () => "Metis: No first-order proof with the lemmas supplied");
    2.84 +            (trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied");
    2.85               [])
    2.86    end;
    2.87  
    2.88 @@ -150,7 +147,7 @@
    2.89  
    2.90  fun generic_metis_tac mode ctxt ths i st0 =
    2.91    let
    2.92 -    val _ = trace_msg (fn () =>
    2.93 +    val _ = trace_msg ctxt (fn () =>
    2.94          "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
    2.95    in
    2.96      if exists_type type_has_top_sort (prop_of st0) then