1.1 --- a/src/Pure/axclass.ML	Thu May 13 20:15:59 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Thu May 13 21:17:09 2010 +0200
     1.3 @@ -196,9 +196,9 @@
     1.4  
     1.5  fun the_classrel thy (c1, c2) =
     1.6    (case Symreltab.lookup (proven_classrels_of thy) (c1, c2) of
     1.7 -    SOME thm => Thm.transfer thy thm
     1.8 +    SOME thm => thm
     1.9    | NONE => error ("Unproven class relation " ^
    1.10 -      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));
    1.11 +      Syntax.string_of_classrel (ProofContext.init_global thy) [c1, c2]));  (* FIXME stale thy (!?) *)
    1.12  
    1.13  fun put_trancl_classrel ((c1, c2), th) thy =
    1.14    let
    1.15 @@ -206,7 +206,7 @@
    1.16      val classrels = proven_classrels_of thy;
    1.17  
    1.18      fun reflcl_classrel (c1', c2') =
    1.19 -      if c1' = c2' then NONE else SOME (the_classrel thy (c1', c2'));
    1.20 +      if c1' = c2' then NONE else SOME (Thm.transfer thy (the_classrel thy (c1', c2')));
    1.21      fun gen_classrel (c1_pred, c2_succ) =
    1.22        let
    1.23          val th' =
    1.24 @@ -243,9 +243,9 @@
    1.25  
    1.26  fun the_arity thy (a, Ss, c) =
    1.27    (case AList.lookup (op =) (Symtab.lookup_list (proven_arities_of thy) a) (c, Ss) of
    1.28 -    SOME (thm, _) => Thm.transfer thy thm
    1.29 +    SOME (thm, _) => thm
    1.30    | NONE => error ("Unproven type arity " ^
    1.31 -      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));
    1.32 +      Syntax.string_of_arity (ProofContext.init_global thy) (a, Ss, [c])));  (* FIXME stale thy (!?) *)
    1.33  
    1.34  fun thynames_of_arity thy (c, a) =
    1.35    Symtab.lookup_list (proven_arities_of thy) a
    1.36 @@ -267,7 +267,7 @@
    1.37      val completions = super_class_completions |> map (fn c1 =>
    1.38        let
    1.39          val th1 =
    1.40 -          (th RS the_classrel thy (c, c1))
    1.41 +          (th RS Thm.transfer thy (the_classrel thy (c, c1)))
    1.42            |> Drule.instantiate' std_vars []
    1.43            |> Thm.close_derivation;
    1.44        in ((th1, thy_name), c1) end);