src/HOL/Tools/res_atp.ML
changeset 21397 2134b81a0b37
parent 21373 18f519614978
child 21431 ef9080e7dbbc
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Nov 16 01:07:39 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Nov 16 17:05:23 2006 +0100
     1.3 @@ -666,10 +666,17 @@
     1.4  
     1.5  val add_type_consts_in_type = fold_type_consts setinsert;
     1.6  
     1.7 -val add_type_consts_in_term = fold_types add_type_consts_in_type;
     1.8 +(*Type constructors used to instantiate overloaded constants are the only ones needed.*)
     1.9 +fun add_type_consts_in_term thy =
    1.10 +  let val const_typargs = Sign.const_typargs thy
    1.11 +      fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
    1.12 +        | add_tcs (Abs (_, T, u)) x = add_tcs u x
    1.13 +        | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
    1.14 +        | add_tcs _ x = x
    1.15 +  in  add_tcs  end
    1.16  
    1.17 -fun type_consts_of_terms ts =
    1.18 -  Symtab.keys (fold add_type_consts_in_term ts Symtab.empty);
    1.19 +fun type_consts_of_terms thy ts =
    1.20 +  Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
    1.21  
    1.22  
    1.23  (***************************************************************)
    1.24 @@ -722,7 +729,7 @@
    1.25          val subs = tfree_classes_of_terms (map prop_of goal_cls)
    1.26          and axtms = map (prop_of o #1) axclauses
    1.27          val supers = tvar_classes_of_terms axtms
    1.28 -        and tycons = type_consts_of_terms axtms
    1.29 +        and tycons = type_consts_of_terms thy axtms
    1.30          (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.31          val classrel_clauses = 
    1.32                if keep_types then ResClause.make_classrel_clauses thy subs supers
    1.33 @@ -854,7 +861,7 @@
    1.34                  val subs = tfree_classes_of_terms (map prop_of ccls)
    1.35                  and axtms = map (prop_of o #1) axcls
    1.36                  val supers = tvar_classes_of_terms axtms
    1.37 -                and tycons = type_consts_of_terms axtms
    1.38 +                and tycons = type_consts_of_terms thy axtms
    1.39                  (*TFrees in conjecture clauses; TVars in axiom clauses*)
    1.40                  val classrel_clauses = 
    1.41                        if keep_types then ResClause.make_classrel_clauses thy subs supers