src/Pure/axclass.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59859 f9d1442c70f3
     1.1 --- a/src/Pure/axclass.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Pure/axclass.ML	Fri Mar 06 15:58:56 2015 +0100
     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.ctyp_of thy2 (TVar ((Name.aT, 0), [])))] []
     1.8 +                |> Drule.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 @@ -228,7 +228,7 @@
    1.13              c1 = c2 andalso Sorts.sorts_le algebra (Ss2, Ss)) ars);
    1.14  
    1.15      val names = Name.invent Name.context Name.aT (length Ss);
    1.16 -    val std_vars = map (fn a => SOME (Thm.ctyp_of thy (TVar ((a, 0), [])))) names;
    1.17 +    val std_vars = map (fn a => SOME (Thm.global_ctyp_of thy (TVar ((a, 0), [])))) names;
    1.18  
    1.19      val completions = super_class_completions |> map (fn c1 =>
    1.20        let
    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.ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
    1.26 +      |> Drule.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 @@ -418,7 +418,7 @@
    1.31  
    1.32      val args = Name.invent_names Name.context Name.aT Ss;
    1.33      val T = Type (t, map TFree args);
    1.34 -    val std_vars = map (fn (a, S) => SOME (Thm.ctyp_of thy' (TVar ((a, 0), [])))) args;
    1.35 +    val std_vars = map (fn (a, S) => SOME (Thm.global_ctyp_of thy' (TVar ((a, 0), [])))) args;
    1.36  
    1.37      val missing_params = Sign.complete_sort thy' [c]
    1.38        |> maps (these o Option.map #params o try (get_info thy'))