1.1 --- a/src/HOL/Tools/primrec.ML	Wed Aug 11 12:24:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 12:30:48 2010 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4  
     1.5  fun add_primrec_overloaded ops fixes specs thy =
     1.6    let
     1.7 -    val lthy = Theory_Target.overloading ops thy;
     1.8 +    val lthy = Overloading.overloading ops thy;
     1.9      val ((ts, simps), lthy') = add_primrec fixes specs lthy;
    1.10      val simps' = ProofContext.export lthy' lthy simps;
    1.11    in ((ts, simps'), Local_Theory.exit_global lthy') end;

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 12:24:24 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 12:30:48 2010 +0200
     2.3 @@ -492,7 +492,7 @@
     2.4        Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
     2.5        >> Parse.triple1) --| Parse.begin
     2.6     >> (fn operations => Toplevel.print o
     2.7 -         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
     2.8 +         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
     2.9  
    2.10  
    2.11  (* code generation *)

     3.1 --- a/src/Pure/Isar/overloading.ML	Wed Aug 11 12:24:24 2010 +0200
     3.2 +++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 12:30:48 2010 +0200
     3.3 @@ -19,6 +19,9 @@
     3.4    val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     3.5      -> Proof.context -> Proof.context
     3.6    val set_primary_constraints: Proof.context -> Proof.context
     3.7 +
     3.8 +  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     3.9 +  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    3.10  end;
    3.11  
    3.12  structure Overloading: OVERLOADING =
    3.13 @@ -194,4 +197,40 @@
    3.14        (Pretty.str "overloading" :: map pr_operation overloading)
    3.15    end;
    3.16  
    3.17 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
    3.18 +
    3.19 +fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    3.20 +  case operation lthy b
    3.21 +   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
    3.22 +        else lthy |> Local_Theory.theory_result (declare (c, U)
    3.23 +            ##>> define checked b_def (c, rhs))
    3.24 +          ||> confirm b
    3.25 +    | NONE => lthy |>
    3.26 +        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    3.27 +
    3.28 +fun gen_overloading prep_const raw_ops thy =
    3.29 +  let
    3.30 +    val ctxt = ProofContext.init_global thy;
    3.31 +    val ops = raw_ops |> map (fn (name, const, checked) =>
    3.32 +      (name, Term.dest_Const (prep_const ctxt const), checked));
    3.33 +  in
    3.34 +    thy
    3.35 +    |> init ops
    3.36 +    |> Local_Theory.init NONE ""
    3.37 +       {define = Generic_Target.define overloading_foundation,
    3.38 +        notes = Generic_Target.notes
    3.39 +          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
    3.40 +        abbrev = Generic_Target.abbrev
    3.41 +          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
    3.42 +            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    3.43 +        declaration = K Generic_Target.theory_declaration,
    3.44 +        syntax_declaration = K Generic_Target.theory_declaration,
    3.45 +        pretty = single o pretty,
    3.46 +        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
    3.47 +        exit = Local_Theory.target_of o conclude}
    3.48 +  end;
    3.49 +
    3.50 +val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    3.51 +val overloading_cmd = gen_overloading Syntax.read_term;
    3.52 +
    3.53  end;

     4.1 --- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:24:24 2010 +0200
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:30:48 2010 +0200
     4.3 @@ -12,8 +12,6 @@
     4.4    val context_cmd: xstring -> theory -> local_theory
     4.5    val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
     4.6    val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
     4.7 -  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
     4.8 -  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
     4.9  end;
    4.10  
    4.11  structure Theory_Target: THEORY_TARGET =
    4.12 @@ -114,15 +112,6 @@
    4.13      | NONE => lthy |>
    4.14          Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    4.15  
    4.16 -fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    4.17 -  case Overloading.operation lthy b
    4.18 -   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
    4.19 -        else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
    4.20 -            ##>> Overloading.define checked b_def (c, rhs))
    4.21 -          ||> Overloading.confirm b
    4.22 -    | NONE => lthy |>
    4.23 -        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
    4.24 -
    4.25  fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
    4.26    if not is_locale then (NoSyn, NoSyn, mx)
    4.27    else if not is_class then (NoSyn, mx, NoSyn)
    4.28 @@ -257,28 +246,6 @@
    4.29        then make_target target true (Class_Target.is_class thy target)
    4.30        else error ("No such locale: " ^ quote target);
    4.31  
    4.32 -fun gen_overloading prep_const raw_ops thy =
    4.33 -  let
    4.34 -    val ctxt = ProofContext.init_global thy;
    4.35 -    val ops = raw_ops |> map (fn (name, const, checked) =>
    4.36 -      (name, Term.dest_Const (prep_const ctxt const), checked));
    4.37 -  in
    4.38 -    thy
    4.39 -    |> Overloading.init ops
    4.40 -    |> Local_Theory.init NONE ""
    4.41 -       {define = Generic_Target.define overloading_foundation,
    4.42 -        notes = Generic_Target.notes
    4.43 -          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
    4.44 -        abbrev = Generic_Target.abbrev
    4.45 -          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
    4.46 -            Generic_Target.theory_abbrev prmode ((b, mx), t)),
    4.47 -        declaration = K Generic_Target.theory_declaration,
    4.48 -        syntax_declaration = K Generic_Target.theory_declaration,
    4.49 -        pretty = single o Overloading.pretty,
    4.50 -        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
    4.51 -        exit = Local_Theory.target_of o Overloading.conclude}
    4.52 -  end;
    4.53 -
    4.54  in
    4.55  
    4.56  fun init target thy = init_target (named_target thy target) thy;
    4.57 @@ -304,9 +271,6 @@
    4.58  fun instantiation_cmd arities thy =
    4.59    instantiation (Class_Target.read_multi_arity thy arities) thy;
    4.60  
    4.61 -val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
    4.62 -val overloading_cmd = gen_overloading Syntax.read_term;
    4.63 -
    4.64  end;
    4.65  
    4.66  end;