--- a/src/Pure/axclass.ML Mon Jul 27 16:35:12 2015 +0200
+++ b/src/Pure/axclass.ML Mon Jul 27 17:44:55 2015 +0200
@@ -191,7 +191,7 @@
thy2
|> update_classrel ((c1, c2),
(the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
|> Thm.close_derivation));
val proven = is_classrel thy1;
@@ -234,7 +234,7 @@
let
val th1 =
(th RS the_classrel thy (c, c1))
- |> Drule.instantiate' std_vars []
+ |> Thm.instantiate' std_vars []
|> Thm.close_derivation;
in ((th1, thy_name), c1) end);
@@ -396,7 +396,7 @@
val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val th'' = th'
|> Thm.unconstrainT
- |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
+ |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
in
thy'
|> Sign.primitive_classrel (c1, c2)
@@ -426,7 +426,7 @@
|> (map o apsnd o map_atyps) (K T);
val th'' = th'
|> Thm.unconstrainT
- |> Drule.instantiate' std_vars [];
+ |> Thm.instantiate' std_vars [];
in
thy'
|> fold (#2 oo declare_overloaded) missing_params