# HG changeset patch
# User wenzelm
# Date 949092943 -3600
# Node ID 27f14e47e2d5f8d66920198b5b6c19dd2072dbc1
# Parent  0b5be7287661386dc698ea2168aef99c78d4fc0c
Drule.instantiate;

diff -r 0b5be7287661 -r 27f14e47e2d5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jan 28 21:55:23 2000 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Jan 28 21:55:43 2000 +0100
@@ -227,7 +227,7 @@
     val cenv =
       map (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t))
         (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
-  in Thm.instantiate (cenvT, cenv) thm end;
+  in Drule.instantiate (cenvT, cenv) thm end;
 
 fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;