removed dead messy code;
authorwenzelm
Fri Jan 30 11:32:19 1998 +0100 (1998-01-30)
changeset 458842bf47c1de1f
parent 4587 6bce9ef27d7e
child 4589 543e867efe40
removed dead messy code;
src/Pure/drule.ML
     1.1 --- a/src/Pure/drule.ML	Fri Jan 30 11:31:21 1998 +0100
     1.2 +++ b/src/Pure/drule.ML	Fri Jan 30 11:32:19 1998 +0100
     1.3 @@ -120,41 +120,6 @@
     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 -      | split((sv,st)::l,tvs,vs) = (case explode sv of
    1.16 -                  "'"::cs => split(l,(indexname cs,st)::tvs,vs)
    1.17 -                | cs => split(l,tvs,(indexname cs,st)::vs));
    1.18 -    val (tvs,vs) = split(insts,[],[]);
    1.19 -    fun readT((a,i),st) =
    1.20 -        let val ixn = ("'" ^ a,i);
    1.21 -            val S = case rsorts ixn of Some S => S | None => absent ixn;
    1.22 -            val T = Sign.read_typ (sign,sorts) st;
    1.23 -        in if Type.typ_instance(tsig,T,TVar(ixn,S)) then (ixn,T)
    1.24 -           else inst_failure ixn
    1.25 -        end
    1.26 -    val tye = map readT tvs;
    1.27 -    fun add_cterm ((cts,tye,used), (ixn,st)) =
    1.28 -        let val T = case rtypes ixn of
    1.29 -                      Some T => typ_subst_TVars tye T
    1.30 -                    | None => absent ixn;
    1.31 -            val (ct,tye2) = read_def_cterm(sign,types,sorts) used false (st,T);
    1.32 -            val cts' = (ixn,T,ct)::cts
    1.33 -            fun inst(ixn,T,ct) = (ixn,typ_subst_TVars tye2 T,ct)
    1.34 -            val used' = add_term_tvarnames(term_of ct,used);
    1.35 -        in (map inst cts',tye2 @ tye,used') end
    1.36 -    val (cterms,tye',_) = foldl add_cterm (([],tye,used), vs);
    1.37 -in (map (fn (ixn,T) => (ixn,ctyp_of sign T)) tye',
    1.38 -    map (fn (ixn,T,ct) => (cterm_of sign (Var(ixn,T)), ct)) cterms)
    1.39 -end;
    1.40 -*)
    1.41 -
    1.42  fun read_insts sign (rtypes,rsorts) (types,sorts) used insts =
    1.43  let val {tsig,...} = Sign.rep_sg sign
    1.44      fun split([],tvs,vs) = (tvs,vs)