--- 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;
--- 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 *)
--- 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;
--- 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;