src/Pure/Isar/rule_insts.ML
changeset 20509 073a5ed7dd71
parent 20487 6ac7a4fc32a0
child 20548 8ef25fe585a8
     1.1 --- a/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:39 2006 +0200
     1.2 +++ b/src/Pure/Isar/rule_insts.ML	Tue Sep 12 12:12:46 2006 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4    end;
     1.5  
     1.6  fun instantiate inst =
     1.7 -  Term.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     1.8 +  TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
     1.9    Envir.beta_norm;
    1.10  
    1.11  fun make_instT f v =
    1.12 @@ -88,7 +88,7 @@
    1.13        end;
    1.14  
    1.15      val type_insts1 = map readT type_insts;
    1.16 -    val instT1 = Term.instantiateT type_insts1;
    1.17 +    val instT1 = TermSubst.instantiateT type_insts1;
    1.18      val vars1 = map (apsnd instT1) vars;
    1.19  
    1.20