src/Pure/drule.ML
changeset 952 9e10962866b0
parent 949 83c588d6fee9
child 1194 563ecd14c1d8
     1.1 --- a/src/Pure/drule.ML	Tue Mar 14 09:47:28 1995 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Mar 14 10:40:04 1995 +0100
     1.3 @@ -249,6 +249,11 @@
     1.4  fun inst_failure ixn =
     1.5    error("Instantiation of " ^ Syntax.string_of_vname ixn ^ " fails");
     1.6  
     1.7 +(* this code is a bit of a mess. add_cterm could be simplified greatly if
     1.8 +   simultaneous instantiations were read or at least type checked
     1.9 +   simultaneously rather than one after the other. This would make the tricky
    1.10 +   composition of implicit type instantiations (parameter tye) superfluous.
    1.11 +*)
    1.12  fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.13  let val {tsig,...} = Sign.rep_sg sign
    1.14      fun split([],tvs,vs) = (tvs,vs)
    1.15 @@ -269,11 +274,14 @@
    1.16                        Some T => typ_subst_TVars tye T
    1.17                      | None => absent ixn;
    1.18              val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
    1.19 -            val cv = cterm_of sign (Var(ixn,typ_subst_TVars tye2 T))
    1.20 +            val cts' = (ixn,T,ct)::cts
    1.21 +            fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
    1.22              val used' = add_term_tvarnames(term_of ct,used);
    1.23 -        in ((cv,ct)::cts,tye2 @ tye,used') end
    1.24 +        in (map inst cts',tye2 @ tye,used') end
    1.25      val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
    1.26 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye', cterms) end;
    1.27 +in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
    1.28 +    map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
    1.29 +end;
    1.30  
    1.31  
    1.32  
    1.33 @@ -585,7 +593,8 @@
    1.34  (*Instantiate theorem th, reading instantiations under signature sg*)
    1.35  fun read_instantiate_sg sg sinsts th =
    1.36      let val ts = types_sorts th;
    1.37 -    in  instantiate (read_insts sg ts ts [] sinsts) th  end;
    1.38 +        val used = add_term_tvarnames(#prop(rep_thm th),[]);
    1.39 +    in  instantiate (read_insts sg ts ts used sinsts) th  end;
    1.40  
    1.41  (*Instantiate theorem th, reading instantiations under theory of th*)
    1.42  fun read_instantiate sinsts th =