1.1 --- a/src/Pure/drule.ML	Mon Jun 16 22:13:46 2008 +0200
     1.2 +++ b/src/Pure/drule.ML	Mon Jun 16 22:13:47 2008 +0200
     1.3 @@ -77,9 +77,6 @@
     1.4    val strip_comb: cterm -> cterm * cterm list
     1.5    val strip_type: ctyp -> ctyp list * ctyp
     1.6    val beta_conv: cterm -> cterm -> cterm
     1.7 -  val read_insts: theory -> (indexname -> typ option) * (indexname -> sort option) ->
     1.8 -    (indexname -> typ option) * (indexname -> sort option) -> string list ->
     1.9 -    (indexname * string) list -> (ctyp * ctyp) list * (cterm * cterm) list
    1.10    val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
    1.11    val add_used: thm -> string list -> string list
    1.12    val flexflex_unique: thm -> thm
    1.13 @@ -103,10 +100,6 @@
    1.14    val protectI: thm
    1.15    val protectD: thm
    1.16    val protect_cong: thm
    1.17 -  val read_instantiate_sg: theory -> (string*string)list -> thm -> thm
    1.18 -  val read_instantiate: (string*string)list -> thm -> thm
    1.19 -  val read_instantiate_sg': theory -> (indexname * string) list -> thm -> thm
    1.20 -  val read_instantiate': (indexname * string) list -> thm -> thm
    1.21    val implies_intr_protected: cterm list -> thm -> thm
    1.22    val termI: thm
    1.23    val mk_term: cterm -> thm
    1.24 @@ -189,44 +182,6 @@
    1.25  
    1.26  
    1.27  
    1.28 -(** reading of instantiations **)
    1.29 -
    1.30 -fun absent ixn =
    1.31 -  error("No such variable in term: " ^ Term.string_of_vname ixn);
    1.32 -
    1.33 -fun inst_failure ixn =
    1.34 -  error("Instantiation of " ^ Term.string_of_vname ixn ^ " fails");
    1.35 -
    1.36 -fun read_insts thy (rtypes,rsorts) (types,sorts) used insts =
    1.37 -let
    1.38 -    fun is_tv ((a, _), _) =
    1.39 -      (case Symbol.explode a of "'" :: _ => true | _ => false);
    1.40 -    val (tvs, vs) = List.partition is_tv insts;
    1.41 -    fun sort_of ixn = case rsorts ixn of SOME S => S | NONE => absent ixn;
    1.42 -    fun readT (ixn, st) =
    1.43 -        let val S = sort_of ixn;
    1.44 -            val T = Sign.read_def_typ (thy,sorts) st;
    1.45 -        in if Sign.typ_instance thy (T, TVar(ixn,S)) then (ixn,T)
    1.46 -           else inst_failure ixn
    1.47 -        end
    1.48 -    val tye = map readT tvs;
    1.49 -    fun mkty(ixn,st) = (case rtypes ixn of
    1.50 -                          SOME T => (ixn,(st,typ_subst_TVars tye T))
    1.51 -                        | NONE => absent ixn);
    1.52 -    val ixnsTs = map mkty vs;
    1.53 -    val ixns = map fst ixnsTs
    1.54 -    and sTs  = map snd ixnsTs
    1.55 -    val (cts,tye2) = Thm.read_def_cterms(thy,types,sorts) used false sTs;
    1.56 -    fun mkcVar(ixn,T) =
    1.57 -        let val U = typ_subst_TVars tye2 T
    1.58 -        in cterm_of thy (Var(ixn,U)) end
    1.59 -    val ixnTs = ListPair.zip(ixns, map snd sTs)
    1.60 -in (map (fn (ixn, T) => (ctyp_of thy (TVar (ixn, sort_of ixn)),
    1.61 -      ctyp_of thy T)) (tye2 @ tye),
    1.62 -    ListPair.zip(map mkcVar ixnTs,cts))
    1.63 -end;
    1.64 -
    1.65 -
    1.66  (*** Find the type (sort) associated with a (T)Var or (T)Free in a term
    1.67       Used for establishing default types (of variables) and sorts (of
    1.68       type variables) when reading another term.
    1.69 @@ -797,22 +752,6 @@
    1.70  fun instantiate instpair th =
    1.71    Thm.adjust_maxidx_thm ~1 (Thm.instantiate instpair th COMP_INCR asm_rl);
    1.72  
    1.73 -fun read_instantiate_sg' thy sinsts th =
    1.74 -    let val ts = types_sorts th;
    1.75 -        val used = add_used th [];
    1.76 -    in  instantiate (read_insts thy ts ts used sinsts) th  end;
    1.77 -
    1.78 -fun read_instantiate_sg thy sinsts th =
    1.79 -  read_instantiate_sg' thy (map (apfst Syntax.read_indexname) sinsts) th;
    1.80 -
    1.81 -(*Instantiate theorem th, reading instantiations under theory of th*)
    1.82 -fun read_instantiate sinsts th =
    1.83 -    read_instantiate_sg (Thm.theory_of_thm th) sinsts th;
    1.84 -
    1.85 -fun read_instantiate' sinsts th =
    1.86 -    read_instantiate_sg' (Thm.theory_of_thm th) sinsts th;
    1.87 -
    1.88 -
    1.89  (*Left-to-right replacements: tpairs = [...,(vi,ti),...].
    1.90    Instantiates distinct Vars by terms, inferring type instantiations. *)
    1.91  local