added polymorphic_types;
authorwenzelm
Mon Sep 24 21:07:39 2007 +0200 (2007-09-24)
changeset 2469454f06f7feefa
parent 24693 fe88913f3706
child 24695 2892482a4e62
added polymorphic_types;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Mon Sep 24 21:07:38 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Mon Sep 24 21:07:39 2007 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context
     1.5    val focus_subgoal: int -> thm -> Proof.context -> (cterm list * cterm) * Proof.context
     1.6    val warn_extra_tfrees: Proof.context -> Proof.context -> unit
     1.7 +  val polymorphic_types: Proof.context -> term list -> (indexname * sort) list * term list
     1.8    val polymorphic: Proof.context -> term list -> term list
     1.9  end;
    1.10  
    1.11 @@ -468,13 +469,20 @@
    1.12  
    1.13  (* polymorphic terms *)
    1.14  
    1.15 -fun polymorphic ctxt ts =
    1.16 +fun polymorphic_types ctxt ts =
    1.17    let
    1.18      val ctxt' = fold declare_term ts ctxt;
    1.19      val occs = type_occs_of ctxt;
    1.20      val occs' = type_occs_of ctxt';
    1.21      val types = Symtab.fold (fn (a, _) => if Symtab.defined occs a then I else cons a) occs' [];
    1.22      val idx = fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1;
    1.23 -  in map (TermSubst.generalize (types, []) idx) ts end;
    1.24 +    val Ts' = (fold o fold_types o fold_atyps)
    1.25 +      (fn T as TFree _ =>
    1.26 +          (case TermSubst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
    1.27 +        | _ => I) ts [];
    1.28 +    val ts' = map (TermSubst.generalize (types, []) idx) ts;
    1.29 +  in (rev Ts', ts') end;
    1.30 +
    1.31 +fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
    1.32  
    1.33  end;