src/Pure/axclass.ML
changeset 60801 7664e0916eec
parent 59859 f9d1442c70f3
child 61246 077b88f9ec16
     1.1 --- a/src/Pure/axclass.ML	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/Pure/axclass.ML	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -191,7 +191,7 @@
     1.4                thy2
     1.5                |> update_classrel ((c1, c2),
     1.6                  (the_classrel thy2 (c1, c) RS the_classrel thy2 (c, c2))
     1.7 -                |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
     1.8 +                |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
     1.9                  |> Thm.close_derivation));
    1.10  
    1.11          val proven = is_classrel thy1;
    1.12 @@ -234,7 +234,7 @@
    1.13        let
    1.14          val th1 =
    1.15            (th RS the_classrel thy (c, c1))
    1.16 -          |> Drule.instantiate' std_vars []
    1.17 +          |> Thm.instantiate' std_vars []
    1.18            |> Thm.close_derivation;
    1.19        in ((th1, thy_name), c1) end);
    1.20  
    1.21 @@ -396,7 +396,7 @@
    1.22      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
    1.23      val th'' = th'
    1.24        |> Thm.unconstrainT
    1.25 -      |> Drule.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
    1.26 +      |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
    1.27    in
    1.28      thy'
    1.29      |> Sign.primitive_classrel (c1, c2)
    1.30 @@ -426,7 +426,7 @@
    1.31        |> (map o apsnd o map_atyps) (K T);
    1.32      val th'' = th'
    1.33        |> Thm.unconstrainT
    1.34 -      |> Drule.instantiate' std_vars [];
    1.35 +      |> Thm.instantiate' std_vars [];
    1.36    in
    1.37      thy'
    1.38      |> fold (#2 oo declare_overloaded) missing_params