src/Pure/Isar/class.ML
changeset 28674 08a77c495dc1
parent 28666 d2dbfe3a0284
child 28715 238f9966c80e
     1.1 --- a/src/Pure/Isar/class.ML	Thu Oct 23 14:22:16 2008 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Thu Oct 23 15:28:01 2008 +0200
     1.3 @@ -497,7 +497,7 @@
     1.4      val ty' = Term.fastype_of dict_def;
     1.5      val ty'' = Type.strip_sorts ty';
     1.6      val def_eq = Logic.mk_equals (Const (c', ty'), dict_def);
     1.7 -    fun get_axiom thy = ((Thm.varifyT o Thm.get_axiom_i thy) c', thy);
     1.8 +    fun get_axiom thy = ((Thm.varifyT o Thm.axiom thy) c', thy);
     1.9    in
    1.10      thy'
    1.11      |> Sign.declare_const pos ((Name.binding c, ty''), mx) |> snd