# HG changeset patch
# User haftmann
# Date 1281529903 -7200
# Node ID cf7b2121ad9dbc81d46c3e6d2e1bfc544feb8204
# Parent  19000bb11ff5d2187f5a1dd792cd5dfd7b2b93ed
moved instantiation target formally to class_target.ML

diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:43 2010 +0200
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
+      |> Class.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -115,7 +115,7 @@
       #> snd
   in
     thy
-    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Class.instantiation (dtcos, vs, [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
          (fn _ => fn def_thms => tac def_thms) def_thms)
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/Function/size.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -145,7 +145,7 @@
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
            (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
-      ||> Theory_Target.instantiation
+      ||> Class.instantiation
            (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
       ||>> fold_map define_overloaded
         (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -86,7 +86,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in   
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
+    |> Class.instantiation ([tyco], vs, @{sort random})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
     |> snd
@@ -304,7 +304,7 @@
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
     thy
-    |> Theory_Target.instantiation (tycos, vs, @{sort random})
+    |> Class.instantiation (tycos, vs, @{sort random})
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -116,7 +116,7 @@
     thy
     |> Code.add_datatype [constr]
     |> Code.add_eqn proj_constr
-    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
+    |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition
          (NONE, (Attrib.empty_binding, eq)))
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Typerep.thy	Wed Aug 11 14:31:43 2010 +0200
@@ -56,7 +56,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
+    |> Class.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOLCF/Tools/pcpodef.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -203,7 +203,7 @@
     val below_eqn = Logic.mk_equals (below_const newT,
       Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
     val lthy3 = thy2
-      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort po});
     val ((_, (_, below_ldef)), lthy4) = lthy3
       |> Specification.definition (NONE,
           ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_eqn));
diff -r 19000bb11ff5 -r cf7b2121ad9d src/HOLCF/Tools/repdef.ML
--- a/src/HOLCF/Tools/repdef.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOLCF/Tools/repdef.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -112,7 +112,7 @@
 
     (*instantiate class rep*)
     val lthy = thy
-      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort rep});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort rep});
     val ((_, (_, emb_ldef)), lthy) =
         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
     val ((_, (_, prj_ldef)), lthy) =
diff -r 19000bb11ff5 -r cf7b2121ad9d src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -47,6 +47,8 @@
   val read_multi_arity: theory -> xstring list * xstring list * xstring
     -> string list * (string * sort) list * sort
   val type_name: string -> string
+  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
+  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
 
   (*subclasses*)
   val register_subclass: class * class -> morphism option -> Element.witness option
@@ -580,6 +582,35 @@
       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case instantiation_param lthy b
+   of SOME c => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
+            ##>> AxClass.define_overloaded b_def (c, rhs))
+          ||> confirm_declaration b
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun instantiation arities thy =
+  thy
+  |> init_instantiation arities
+  |> Local_Theory.init NONE ""
+     {define = Generic_Target.define instantiation_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_instantiation,
+      reinit = instantiation arities o ProofContext.theory_of,
+      exit = Local_Theory.target_of o conclude_instantiation};
+
+fun instantiation_cmd arities thy =
+  instantiation (read_multi_arity thy arities) thy;
+
 
 (* simplified instantiation interface with no class parameter *)
 
diff -r 19000bb11ff5 -r cf7b2121ad9d src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -472,7 +472,7 @@
   Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
    (Parse.multi_arity --| Parse.begin
      >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
+         Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
 
 val _ =
   Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
diff -r 19000bb11ff5 -r cf7b2121ad9d src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/theory_target.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -10,8 +10,6 @@
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
   val init: string option -> theory -> local_theory
   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
 end;
 
 structure Theory_Target: THEORY_TARGET =
@@ -89,8 +87,6 @@
 
 (* define *)
 
-fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
-
 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
   #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
@@ -103,14 +99,7 @@
     #> class_target ta (Class_Target.declare target ((b, mx), (type_params, lhs)))
     #> pair (lhs, def))
 
-fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
-  case Class_Target.instantiation_param lthy b
-   of SOME c => if mx <> NoSyn then syntax_error c
-        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
-            ##>> AxClass.define_overloaded b_def (c, rhs))
-          ||> Class_Target.confirm_declaration b
-    | NONE => lthy |>
-        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
 
 fun fork_mixfix (Target {is_locale, is_class, ...}) mx =
   if not is_locale then (NoSyn, NoSyn, mx)
@@ -253,24 +242,6 @@
 fun context_cmd "-" thy = init NONE thy
   | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
 
-fun instantiation arities thy =
-  thy
-  |> Class_Target.init_instantiation arities
-  |> Local_Theory.init NONE ""
-     {define = Generic_Target.define instantiation_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 Class_Target.pretty_instantiation,
-      reinit = instantiation arities o ProofContext.theory_of,
-      exit = Local_Theory.target_of o Class_Target.conclude_instantiation};
-
-fun instantiation_cmd arities thy =
-  instantiation (Class_Target.read_multi_arity thy arities) thy;
-
 end;
 
 end;