src/Pure/Isar/theory_target.ML
changeset 25597 34860182b250
parent 25542 ced4104f6c1f
child 25607 779c79c36c5e
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Dec 10 11:24:14 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Dec 10 11:24:15 2007 +0100
     1.3 @@ -203,7 +203,7 @@
     1.4      fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
     1.5      val declare_const = case Class.instantiation_param lthy c
     1.6         of SOME c' => if mx3 <> NoSyn then syntax_error c'
     1.7 -          else LocalTheory.theory_result (Class.overloaded_const (c', U))
     1.8 +          else LocalTheory.theory_result (AxClass.declare_overloaded (c', U))
     1.9              ##> Class.confirm_declaration c
    1.10          | NONE => (case Overloading.operation lthy c
    1.11             of SOME (c', _) => if mx3 <> NoSyn then syntax_error c'
    1.12 @@ -276,7 +276,7 @@
    1.13            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
    1.14        | NONE => if is_none (Class.instantiation_param lthy c)
    1.15            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
    1.16 -          else (fn name => fn (Const (c, _), rhs) => Class.overloaded_def name (c, rhs));
    1.17 +          else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs));
    1.18      val (global_def, lthy3) = lthy2
    1.19        |> LocalTheory.theory_result (define_const name' (lhs', rhs'));
    1.20      val def = LocalDefs.trans_terms lthy3