src/HOL/Tools/Sledgehammer/metis_clauses.ML
author blanchet
Tue Aug 24 22:57:22 2010 +0200 (2010-08-24)
changeset 38738 0ce517c1970f
parent 38653 78d0f18d5b36
child 38748 69fea359d3f8
permissions -rw-r--r--
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
     1 (*  Title:      HOL/Tools/Sledgehammer/metis_clauses.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 Storing/printing FOL clauses and arity clauses.  Typed equality is
     6 treated differently.
     7 *)
     8 
     9 signature METIS_CLAUSES =
    10 sig
    11   type name = string * string
    12   datatype type_literal =
    13     TyLitVar of name * name |
    14     TyLitFree of name * name
    15   datatype arLit =
    16     TConsLit of name * name * name list |
    17     TVarLit of name * name
    18   datatype arity_clause =
    19     ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
    20   datatype class_rel_clause =
    21     ClassRelClause of {name: string, subclass: name, superclass: name}
    22   datatype combtyp =
    23     CombTVar of name |
    24     CombTFree of name |
    25     CombType of name * combtyp list
    26   datatype combterm =
    27     CombConst of name * combtyp * combtyp list (* Const and Free *) |
    28     CombVar of name * combtyp |
    29     CombApp of combterm * combterm
    30   datatype fol_literal = FOLLiteral of bool * combterm
    31 
    32   val type_wrapper_name : string
    33   val bound_var_prefix : string
    34   val schematic_var_prefix: string
    35   val fixed_var_prefix: string
    36   val tvar_prefix: string
    37   val tfree_prefix: string
    38   val const_prefix: string
    39   val type_const_prefix: string
    40   val class_prefix: string
    41   val union_all: ''a list list -> ''a list
    42   val invert_const: string -> string
    43   val ascii_of: string -> string
    44   val undo_ascii_of: string -> string
    45   val strip_prefix_and_undo_ascii: string -> string -> string option
    46   val make_bound_var : string -> string
    47   val make_schematic_var : string * int -> string
    48   val make_fixed_var : string -> string
    49   val make_schematic_type_var : string * int -> string
    50   val make_fixed_type_var : string -> string
    51   val make_fixed_const : string -> string
    52   val make_fixed_type_const : string -> string
    53   val make_type_class : string -> string
    54   val skolem_theory_name: string
    55   val skolem_prefix: string
    56   val skolem_infix: string
    57   val is_skolem_const_name: string -> bool
    58   val num_type_args: theory -> string -> int
    59   val type_literals_for_types : typ list -> type_literal list
    60   val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
    61   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
    62   val combtyp_of : combterm -> combtyp
    63   val strip_combterm_comb : combterm -> combterm * combterm list
    64   val combterm_from_term :
    65     theory -> (string * typ) list -> term -> combterm * typ list
    66   val literals_of_term : theory -> term -> fol_literal list * typ list
    67   val conceal_skolem_terms :
    68     int -> (string * term) list -> term -> (string * term) list * term
    69   val reveal_skolem_terms : (string * term) list -> term -> term
    70   val tfree_classes_of_terms : term list -> string list
    71   val tvar_classes_of_terms : term list -> string list
    72   val type_consts_of_terms : theory -> term list -> string list
    73 end
    74 
    75 structure Metis_Clauses : METIS_CLAUSES =
    76 struct
    77 
    78 val type_wrapper_name = "ti"
    79 
    80 val bound_var_prefix = "B_"
    81 val schematic_var_prefix = "V_"
    82 val fixed_var_prefix = "v_"
    83 
    84 val tvar_prefix = "T_";
    85 val tfree_prefix = "t_";
    86 
    87 val const_prefix = "c_";
    88 val type_const_prefix = "tc_";
    89 val class_prefix = "class_";
    90 
    91 fun union_all xss = fold (union (op =)) xss []
    92 
    93 (* Readable names for the more common symbolic functions. Do not mess with the
    94    last nine entries of the table unless you know what you are doing. *)
    95 val const_trans_table =
    96   Symtab.make [(@{type_name Product_Type.prod}, "prod"),
    97                (@{type_name Sum_Type.sum}, "sum"),
    98                (@{const_name "op ="}, "equal"),
    99                (@{const_name "op &"}, "and"),
   100                (@{const_name "op |"}, "or"),
   101                (@{const_name "op -->"}, "implies"),
   102                (@{const_name Set.member}, "member"),
   103                (@{const_name fequal}, "fequal"),
   104                (@{const_name COMBI}, "COMBI"),
   105                (@{const_name COMBK}, "COMBK"),
   106                (@{const_name COMBB}, "COMBB"),
   107                (@{const_name COMBC}, "COMBC"),
   108                (@{const_name COMBS}, "COMBS"),
   109                (@{const_name True}, "True"),
   110                (@{const_name False}, "False"),
   111                (@{const_name If}, "If")]
   112 
   113 (* Invert the table of translations between Isabelle and ATPs. *)
   114 val const_trans_table_inv =
   115   Symtab.update ("fequal", @{const_name "op ="})
   116                 (Symtab.make (map swap (Symtab.dest const_trans_table)))
   117 
   118 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   119 
   120 (*Escaping of special characters.
   121   Alphanumeric characters are left unchanged.
   122   The character _ goes to __
   123   Characters in the range ASCII space to / go to _A to _P, respectively.
   124   Other characters go to _nnn where nnn is the decimal ASCII code.*)
   125 val A_minus_space = Char.ord #"A" - Char.ord #" ";
   126 
   127 fun stringN_of_int 0 _ = ""
   128   | stringN_of_int k n = stringN_of_int (k-1) (n div 10) ^ Int.toString (n mod 10);
   129 
   130 fun ascii_of_c c =
   131   if Char.isAlphaNum c then String.str c
   132   else if c = #"_" then "__"
   133   else if #" " <= c andalso c <= #"/"
   134        then "_" ^ String.str (Char.chr (Char.ord c + A_minus_space))
   135   else ("_" ^ stringN_of_int 3 (Char.ord c))  (*fixed width, in case more digits follow*)
   136 
   137 val ascii_of = String.translate ascii_of_c;
   138 
   139 (** Remove ASCII armouring from names in proof files **)
   140 
   141 (*We don't raise error exceptions because this code can run inside the watcher.
   142   Also, the errors are "impossible" (hah!)*)
   143 fun undo_ascii_aux rcs [] = String.implode(rev rcs)
   144   | undo_ascii_aux rcs [#"_"] = undo_ascii_aux (#"_"::rcs) []  (*ERROR*)
   145       (*Three types of _ escapes: __, _A to _P, _nnn*)
   146   | undo_ascii_aux rcs (#"_" :: #"_" :: cs) = undo_ascii_aux (#"_"::rcs) cs
   147   | undo_ascii_aux rcs (#"_" :: c :: cs) =
   148       if #"A" <= c andalso c<= #"P"  (*translation of #" " to #"/"*)
   149       then undo_ascii_aux (Char.chr(Char.ord c - A_minus_space) :: rcs) cs
   150       else
   151         let val digits = List.take (c::cs, 3) handle Subscript => []
   152         in
   153             case Int.fromString (String.implode digits) of
   154                 NONE => undo_ascii_aux (c:: #"_"::rcs) cs  (*ERROR*)
   155               | SOME n => undo_ascii_aux (Char.chr n :: rcs) (List.drop (cs, 2))
   156         end
   157   | undo_ascii_aux rcs (c::cs) = undo_ascii_aux (c::rcs) cs;
   158 
   159 val undo_ascii_of = undo_ascii_aux [] o String.explode;
   160 
   161 (* If string s has the prefix s1, return the result of deleting it,
   162    un-ASCII'd. *)
   163 fun strip_prefix_and_undo_ascii s1 s =
   164   if String.isPrefix s1 s then
   165     SOME (undo_ascii_of (String.extract (s, size s1, NONE)))
   166   else
   167     NONE
   168 
   169 (*Remove the initial ' character from a type variable, if it is present*)
   170 fun trim_type_var s =
   171   if s <> "" andalso String.sub(s,0) = #"'" then String.extract(s,1,NONE)
   172   else error ("trim_type: Malformed type variable encountered: " ^ s);
   173 
   174 fun ascii_of_indexname (v,0) = ascii_of v
   175   | ascii_of_indexname (v,i) = ascii_of v ^ "_" ^ Int.toString i;
   176 
   177 fun make_bound_var x = bound_var_prefix ^ ascii_of x
   178 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   179 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   180 
   181 fun make_schematic_type_var (x,i) =
   182       tvar_prefix ^ (ascii_of_indexname (trim_type_var x,i));
   183 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (trim_type_var x));
   184 
   185 fun lookup_const c =
   186   case Symtab.lookup const_trans_table c of
   187     SOME c' => c'
   188   | NONE => ascii_of c
   189 
   190 (* "op =" MUST BE "equal" because it's built into ATPs. *)
   191 fun make_fixed_const @{const_name "op ="} = "equal"
   192   | make_fixed_const c = const_prefix ^ lookup_const c
   193 
   194 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   195 
   196 fun make_type_class clas = class_prefix ^ ascii_of clas;
   197 
   198 val skolem_theory_name = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
   199 val skolem_prefix = "sko_"
   200 val skolem_infix = "$"
   201 
   202 (* Hack: Could return false positives (e.g., a user happens to declare a
   203    constant called "SomeTheory.sko_means_shoe_in_$wedish". *)
   204 val is_skolem_const_name =
   205   Long_Name.base_name
   206   #> String.isPrefix skolem_prefix andf String.isSubstring skolem_infix
   207 
   208 (* The number of type arguments of a constant, zero if it's monomorphic. For
   209    (instances of) Skolem pseudoconstants, this information is encoded in the
   210    constant name. *)
   211 fun num_type_args thy s =
   212   if String.isPrefix skolem_theory_name s then
   213     s |> unprefix skolem_theory_name
   214       |> space_explode skolem_infix |> hd
   215       |> space_explode "_" |> List.last |> Int.fromString |> the
   216   else
   217     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
   218 
   219 (**** Definitions and functions for FOL clauses for TPTP format output ****)
   220 
   221 type name = string * string
   222 
   223 (**** Isabelle FOL clauses ****)
   224 
   225 (* The first component is the type class; the second is a TVar or TFree. *)
   226 datatype type_literal =
   227   TyLitVar of name * name |
   228   TyLitFree of name * name
   229 
   230 exception CLAUSE of string * term;
   231 
   232 (*Make literals for sorted type variables*)
   233 fun sorts_on_typs_aux (_, [])   = []
   234   | sorts_on_typs_aux ((x,i),  s::ss) =
   235       let val sorts = sorts_on_typs_aux ((x,i), ss)
   236       in
   237           if s = "HOL.type" then sorts
   238           else if i = ~1 then TyLitFree (`make_type_class s, `make_fixed_type_var x) :: sorts
   239           else TyLitVar (`make_type_class s, (make_schematic_type_var (x,i), x)) :: sorts
   240       end;
   241 
   242 fun sorts_on_typs (TFree (a,s)) = sorts_on_typs_aux ((a,~1),s)
   243   | sorts_on_typs (TVar (v,s))  = sorts_on_typs_aux (v,s);
   244 
   245 (*Given a list of sorted type variables, return a list of type literals.*)
   246 fun type_literals_for_types Ts =
   247   fold (union (op =)) (map sorts_on_typs Ts) []
   248 
   249 (** make axiom and conjecture clauses. **)
   250 
   251 (**** Isabelle arities ****)
   252 
   253 datatype arLit =
   254   TConsLit of name * name * name list |
   255   TVarLit of name * name
   256 
   257 datatype arity_clause =
   258   ArityClause of {name: string, conclLit: arLit, premLits: arLit list}
   259 
   260 
   261 fun gen_TVars 0 = []
   262   | gen_TVars n = ("T_" ^ Int.toString n) :: gen_TVars (n-1);
   263 
   264 fun pack_sort(_,[])  = []
   265   | pack_sort(tvar, "HOL.type"::srt) = pack_sort (tvar, srt)   (*IGNORE sort "type"*)
   266   | pack_sort(tvar, cls::srt) =
   267     (`make_type_class cls, (tvar, tvar)) :: pack_sort (tvar, srt)
   268 
   269 (*Arity of type constructor tcon :: (arg1,...,argN)res*)
   270 fun make_axiom_arity_clause (tcons, name, (cls,args)) =
   271   let
   272     val tvars = gen_TVars (length args)
   273     val tvars_srts = ListPair.zip (tvars, args)
   274   in
   275     ArityClause {name = name, 
   276                  conclLit = TConsLit (`make_type_class cls,
   277                                       `make_fixed_type_const tcons,
   278                                       tvars ~~ tvars),
   279                  premLits = map TVarLit (union_all (map pack_sort tvars_srts))}
   280   end
   281 
   282 
   283 (**** Isabelle class relations ****)
   284 
   285 datatype class_rel_clause =
   286   ClassRelClause of {name: string, subclass: name, superclass: name}
   287 
   288 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
   289 fun class_pairs _ [] _ = []
   290   | class_pairs thy subs supers =
   291       let
   292         val class_less = Sorts.class_less (Sign.classes_of thy)
   293         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   294         fun add_supers sub = fold (add_super sub) supers
   295       in fold add_supers subs [] end
   296 
   297 fun make_class_rel_clause (sub,super) =
   298   ClassRelClause {name = sub ^ "_" ^ super,
   299                   subclass = `make_type_class sub,
   300                   superclass = `make_type_class super}
   301 
   302 fun make_class_rel_clauses thy subs supers =
   303   map make_class_rel_clause (class_pairs thy subs supers);
   304 
   305 
   306 (** Isabelle arities **)
   307 
   308 fun arity_clause _ _ (_, []) = []
   309   | arity_clause seen n (tcons, ("HOL.type",_)::ars) =  (*ignore*)
   310       arity_clause seen n (tcons,ars)
   311   | arity_clause seen n (tcons, (ar as (class,_)) :: ars) =
   312       if member (op =) seen class then (*multiple arities for the same tycon, class pair*)
   313           make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class ^ "_" ^ Int.toString n, ar) ::
   314           arity_clause seen (n+1) (tcons,ars)
   315       else
   316           make_axiom_arity_clause (tcons, lookup_const tcons ^ "_" ^ class, ar) ::
   317           arity_clause (class::seen) n (tcons,ars)
   318 
   319 fun multi_arity_clause [] = []
   320   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   321       arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   322 
   323 (*Generate all pairs (tycon,class,sorts) such that tycon belongs to class in theory thy
   324   provided its arguments have the corresponding sorts.*)
   325 fun type_class_pairs thy tycons classes =
   326   let val alg = Sign.classes_of thy
   327       fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   328       fun add_class tycon class =
   329         cons (class, domain_sorts tycon class)
   330         handle Sorts.CLASS_ERROR _ => I
   331       fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   332   in  map try_classes tycons  end;
   333 
   334 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   335 fun iter_type_class_pairs _ _ [] = ([], [])
   336   | iter_type_class_pairs thy tycons classes =
   337       let val cpairs = type_class_pairs thy tycons classes
   338           val newclasses = union_all (union_all (union_all (map (map #2 o #2) cpairs)))
   339             |> subtract (op =) classes |> subtract (op =) HOLogic.typeS
   340           val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   341       in (union (op =) classes' classes, union (op =) cpairs' cpairs) end;
   342 
   343 fun make_arity_clauses thy tycons classes =
   344   let val (classes', cpairs) = iter_type_class_pairs thy tycons classes
   345   in  (classes', multi_arity_clause cpairs)  end;
   346 
   347 datatype combtyp =
   348   CombTVar of name |
   349   CombTFree of name |
   350   CombType of name * combtyp list
   351 
   352 datatype combterm =
   353   CombConst of name * combtyp * combtyp list (* Const and Free *) |
   354   CombVar of name * combtyp |
   355   CombApp of combterm * combterm
   356 
   357 datatype fol_literal = FOLLiteral of bool * combterm
   358 
   359 (*********************************************************************)
   360 (* convert a clause with type Term.term to a clause with type clause *)
   361 (*********************************************************************)
   362 
   363 (*Result of a function type; no need to check that the argument type matches.*)
   364 fun result_type (CombType (_, [_, tp2])) = tp2
   365   | result_type _ = raise Fail "non-function type"
   366 
   367 fun combtyp_of (CombConst (_, tp, _)) = tp
   368   | combtyp_of (CombVar (_, tp)) = tp
   369   | combtyp_of (CombApp (t1, _)) = result_type (combtyp_of t1)
   370 
   371 (*gets the head of a combinator application, along with the list of arguments*)
   372 fun strip_combterm_comb u =
   373     let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
   374         |   stripc  x =  x
   375     in stripc(u,[]) end
   376 
   377 fun type_of (Type (a, Ts)) =
   378     let val (folTypes,ts) = types_of Ts in
   379       (CombType (`make_fixed_type_const a, folTypes), ts)
   380     end
   381   | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
   382   | type_of (tp as TVar (x, _)) =
   383     (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
   384 and types_of Ts =
   385     let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
   386       (folTyps, union_all ts)
   387     end
   388 
   389 (* same as above, but no gathering of sort information *)
   390 fun simp_type_of (Type (a, Ts)) =
   391       CombType (`make_fixed_type_const a, map simp_type_of Ts)
   392   | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
   393   | simp_type_of (TVar (x, _)) =
   394     CombTVar (make_schematic_type_var x, string_of_indexname x)
   395 
   396 (* Converts a term (with combinators) into a combterm. Also accummulates sort
   397    infomation. *)
   398 fun combterm_from_term thy bs (P $ Q) =
   399       let val (P', tsP) = combterm_from_term thy bs P
   400           val (Q', tsQ) = combterm_from_term thy bs Q
   401       in  (CombApp (P', Q'), union (op =) tsP tsQ)  end
   402   | combterm_from_term thy _ (Const (c, T)) =
   403       let
   404         val (tp, ts) = type_of T
   405         val tvar_list =
   406           (if String.isPrefix skolem_theory_name c then
   407              [] |> Term.add_tvarsT T |> map TVar
   408            else
   409              (c, T) |> Sign.const_typargs thy)
   410           |> map simp_type_of
   411         val c' = CombConst (`make_fixed_const c, tp, tvar_list)
   412       in  (c',ts)  end
   413   | combterm_from_term _ _ (Free (v, T)) =
   414       let val (tp,ts) = type_of T
   415           val v' = CombConst (`make_fixed_var v, tp, [])
   416       in  (v',ts)  end
   417   | combterm_from_term _ _ (Var (v, T)) =
   418       let val (tp,ts) = type_of T
   419           val v' = CombVar ((make_schematic_var v, string_of_indexname v), tp)
   420       in  (v',ts)  end
   421   | combterm_from_term _ bs (Bound j) =
   422       let
   423         val (s, T) = nth bs j
   424         val (tp, ts) = type_of T
   425         val v' = CombConst (`make_bound_var s, tp, [])
   426       in (v', ts) end
   427   | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
   428 
   429 fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
   430   | predicate_of thy (t, pos) =
   431     (combterm_from_term thy [] (Envir.eta_contract t), pos)
   432 
   433 fun literals_of_term1 args thy (@{const Trueprop} $ P) =
   434     literals_of_term1 args thy P
   435   | literals_of_term1 args thy (@{const "op |"} $ P $ Q) =
   436     literals_of_term1 (literals_of_term1 args thy P) thy Q
   437   | literals_of_term1 (lits, ts) thy P =
   438     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
   439       (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
   440     end
   441 val literals_of_term = literals_of_term1 ([], [])
   442 
   443 fun skolem_name i j num_T_args =
   444   skolem_prefix ^ (space_implode "_" (map Int.toString [i, j, num_T_args])) ^
   445   skolem_infix ^ "g"
   446 
   447 fun conceal_skolem_terms i skolems t =
   448   if exists_Const (curry (op =) @{const_name skolem_id} o fst) t then
   449     let
   450       fun aux skolems
   451               (t as (Const (@{const_name skolem_id}, Type (_, [_, T])) $ _)) =
   452           let
   453             val (skolems, s) =
   454               if i = ~1 then
   455                 (skolems, @{const_name undefined})
   456               else case AList.find (op aconv) skolems t of
   457                 s :: _ => (skolems, s)
   458               | [] =>
   459                 let
   460                   val s = skolem_theory_name ^ "." ^
   461                           skolem_name i (length skolems)
   462                                         (length (Term.add_tvarsT T []))
   463                 in ((s, t) :: skolems, s) end
   464           in (skolems, Const (s, T)) end
   465         | aux skolems (t1 $ t2) =
   466           let
   467             val (skolems, t1) = aux skolems t1
   468             val (skolems, t2) = aux skolems t2
   469           in (skolems, t1 $ t2) end
   470         | aux skolems (Abs (s, T, t')) =
   471           let val (skolems, t') = aux skolems t' in
   472             (skolems, Abs (s, T, t'))
   473           end
   474         | aux skolems t = (skolems, t)
   475     in aux skolems t end
   476   else
   477     (skolems, t)
   478 
   479 fun reveal_skolem_terms skolems =
   480   map_aterms (fn t as Const (s, _) =>
   481                  if String.isPrefix skolem_theory_name s then
   482                    AList.lookup (op =) skolems s |> the
   483                    |> map_types Type_Infer.paramify_vars
   484                  else
   485                    t
   486                | t => t)
   487 
   488 
   489 (***************************************************************)
   490 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   491 (***************************************************************)
   492 
   493 fun set_insert (x, s) = Symtab.update (x, ()) s
   494 
   495 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
   496 
   497 (*Remove this trivial type class*)
   498 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset;
   499 
   500 fun tfree_classes_of_terms ts =
   501   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   502   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   503 
   504 fun tvar_classes_of_terms ts =
   505   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   506   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   507 
   508 (*fold type constructors*)
   509 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   510   | fold_type_consts _ _ x = x;
   511 
   512 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   513 fun add_type_consts_in_term thy =
   514   let
   515     val const_typargs = Sign.const_typargs thy
   516     fun aux (Const x) = fold (fold_type_consts set_insert) (const_typargs x)
   517       | aux (Abs (_, _, u)) = aux u
   518       | aux (Const (@{const_name skolem_id}, _) $ _) = I
   519       | aux (t $ u) = aux t #> aux u
   520       | aux _ = I
   521   in aux end
   522 
   523 fun type_consts_of_terms thy ts =
   524   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   525 
   526 end;