# HG changeset patch
# User haftmann
# Date 1281522648 -7200
# Node ID 09d4a04d5c2efefe414806bbc94f030ddddff31c
# Parent  72dba5bd5f631f2b5adaee2c7245fdd17656f0b4
moved overloading target formally to overloading.ML

diff -r 72dba5bd5f63 -r 09d4a04d5c2e src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Wed Aug 11 12:24:24 2010 +0200
+++ b/src/HOL/Tools/primrec.ML	Wed Aug 11 12:30:48 2010 +0200
@@ -299,7 +299,7 @@
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
-    val lthy = Theory_Target.overloading ops thy;
+    val lthy = Overloading.overloading ops thy;
     val ((ts, simps), lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in ((ts, simps'), Local_Theory.exit_global lthy') end;
diff -r 72dba5bd5f63 -r 09d4a04d5c2e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 12:24:24 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 12:30:48 2010 +0200
@@ -492,7 +492,7 @@
       Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
       >> Parse.triple1) --| Parse.begin
    >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
+         Toplevel.begin_local_theory true (Overloading.overloading_cmd operations)));
 
 
 (* code generation *)
diff -r 72dba5bd5f63 -r 09d4a04d5c2e src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Aug 11 12:24:24 2010 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Aug 11 12:30:48 2010 +0200
@@ -19,6 +19,9 @@
   val map_improvable_syntax: (improvable_syntax -> improvable_syntax)
     -> Proof.context -> Proof.context
   val set_primary_constraints: Proof.context -> Proof.context
+
+  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
+  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;
 
 structure Overloading: OVERLOADING =
@@ -194,4 +197,40 @@
       (Pretty.str "overloading" :: map pr_operation overloading)
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case operation lthy b
+   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (declare (c, U)
+            ##>> define checked b_def (c, rhs))
+          ||> confirm b
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun gen_overloading prep_const raw_ops thy =
+  let
+    val ctxt = ProofContext.init_global thy;
+    val ops = raw_ops |> map (fn (name, const, checked) =>
+      (name, Term.dest_Const (prep_const ctxt const), checked));
+  in
+    thy
+    |> init ops
+    |> Local_Theory.init NONE ""
+       {define = Generic_Target.define overloading_foundation,
+        notes = Generic_Target.notes
+          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+        abbrev = Generic_Target.abbrev
+          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
+            Generic_Target.theory_abbrev prmode ((b, mx), t)),
+        declaration = K Generic_Target.theory_declaration,
+        syntax_declaration = K Generic_Target.theory_declaration,
+        pretty = single o pretty,
+        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
+        exit = Local_Theory.target_of o conclude}
+  end;
+
+val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
+val overloading_cmd = gen_overloading Syntax.read_term;
+
 end;
diff -r 72dba5bd5f63 -r 09d4a04d5c2e src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:24:24 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 12:30:48 2010 +0200
@@ -12,8 +12,6 @@
   val context_cmd: xstring -> theory -> local_theory
   val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
   val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
-  val overloading: (string * (string * typ) * bool) list -> theory -> local_theory
-  val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;
 
 structure Theory_Target: THEORY_TARGET =
@@ -114,15 +112,6 @@
     | NONE => lthy |>
         Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
 
-fun overloading_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case Overloading.operation lthy b
-   of SOME (c, checked) => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (Overloading.declare (c, U)
-            ##>> Overloading.define checked b_def (c, rhs))
-          ||> Overloading.confirm b
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
-
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
   else if not is_class then (NoSyn, mx, NoSyn)
@@ -257,28 +246,6 @@
       then make_target target true (Class_Target.is_class thy target)
       else error ("No such locale: " ^ quote target);
 
-fun gen_overloading prep_const raw_ops thy =
-  let
-    val ctxt = ProofContext.init_global thy;
-    val ops = raw_ops |> map (fn (name, const, checked) =>
-      (name, Term.dest_Const (prep_const ctxt const), checked));
-  in
-    thy
-    |> Overloading.init ops
-    |> Local_Theory.init NONE ""
-       {define = Generic_Target.define overloading_foundation,
-        notes = Generic_Target.notes
-          (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
-        abbrev = Generic_Target.abbrev
-          (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
-            Generic_Target.theory_abbrev prmode ((b, mx), t)),
-        declaration = K Generic_Target.theory_declaration,
-        syntax_declaration = K Generic_Target.theory_declaration,
-        pretty = single o Overloading.pretty,
-        reinit = gen_overloading prep_const raw_ops o ProofContext.theory_of,
-        exit = Local_Theory.target_of o Overloading.conclude}
-  end;
-
 in
 
 fun init target thy = init_target (named_target thy target) thy;
@@ -304,9 +271,6 @@
 fun instantiation_cmd arities thy =
   instantiation (Class_Target.read_multi_arity thy arities) thy;
 
-val overloading = gen_overloading (fn ctxt => Syntax.check_term ctxt o Const);
-val overloading_cmd = gen_overloading Syntax.read_term;
-
 end;
 
 end;