# HG changeset patch
# User wenzelm
# Date 1257865497 -3600
# Node ID 35f2b30593a8dcb445ea0d6d2d182a098453c561
# Parent  506f80a9afe805bf7a4c0ac37e2ab25bef15ec90
modernized structure Theory_Target;

diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOL/Code_Evaluation.thy
--- a/src/HOL/Code_Evaluation.thy	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Code_Evaluation.thy	Tue Nov 10 16:04:57 2009 +0100
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
+      |> Theory_Target.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 506f80a9afe8 -r 35f2b30593a8 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -349,7 +349,7 @@
 
 fun add_declaration name decl thy =
   thy
-  |> TheoryTarget.init name
+  |> Theory_Target.init name
   |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
   |> LocalTheory.exit_global;
 
diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -411,7 +411,7 @@
         #> fold_rev Code.add_eqn thms);
   in
     thy
-    |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
+    |> Theory_Target.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 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/Function/size.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -144,7 +144,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)))
-      ||> TheoryTarget.instantiation
+      ||> Theory_Target.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 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -895,7 +895,7 @@
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
-      |> TheoryTarget.init NONE
+      |> Theory_Target.init NONE
       |> LocalTheory.set_group group
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> LocalTheory.exit;
diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -293,14 +293,14 @@
 
 fun add_primrec_global fixes specs thy =
   let
-    val lthy = TheoryTarget.init NONE thy;
+    val lthy = Theory_Target.init NONE thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in (simps', LocalTheory.exit_global lthy') end;
 
 fun add_primrec_overloaded ops fixes specs thy =
   let
-    val lthy = TheoryTarget.overloading ops thy;
+    val lthy = Theory_Target.overloading ops thy;
     val (simps, lthy') = add_primrec fixes specs lthy;
     val simps' = ProofContext.export lthy' lthy simps;
   in (simps', LocalTheory.exit_global lthy') end;
diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -82,7 +82,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in   
     thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
+    |> Theory_Target.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
@@ -300,7 +300,7 @@
       (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
   in
     thy
-    |> TheoryTarget.instantiation (tycos, vs, @{sort random})
+    |> Theory_Target.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 506f80a9afe8 -r 35f2b30593a8 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Tools/typecopy.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -113,7 +113,7 @@
     thy
     |> Code.add_datatype [constr]
     |> Code.add_eqn proj_eq
-    |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
+    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition
          (NONE, (Attrib.empty_binding, eq)))
diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOL/Typerep.thy	Tue Nov 10 16:04:57 2009 +0100
@@ -50,7 +50,7 @@
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
-    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
+    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
     |> snd
diff -r 506f80a9afe8 -r 35f2b30593a8 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -75,7 +75,7 @@
         val ((_, {type_definition, set_def, ...}), thy2) = thy1
           |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
         val lthy3 = thy2
-          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
+          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
         val below_def' = Syntax.check_term lthy3 below_def;
         val ((_, (_, below_definition')), lthy4) = lthy3
           |> Specification.definition (NONE,
diff -r 506f80a9afe8 -r 35f2b30593a8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/Pure/Isar/class.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -290,7 +290,7 @@
        Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
          (*FIXME should not modify base_morph, although admissible*)
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
-    |> TheoryTarget.init (SOME class)
+    |> Theory_Target.init (SOME class)
     |> pair class
   end;
 
@@ -310,7 +310,7 @@
   let
     val thy = ProofContext.theory_of lthy;
     val proto_sup = prep_class thy raw_sup;
-    val proto_sub = case TheoryTarget.peek lthy
+    val proto_sub = case Theory_Target.peek lthy
      of {is_class = false, ...} => error "Not in a class context"
       | {target, ...} => target;
     val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
@@ -323,7 +323,7 @@
     fun after_qed some_wit =
       ProofContext.theory (register_subclass (sub, sup)
         some_dep_morph some_wit export)
-      #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
+      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
   in do_proof after_qed some_prop goal_ctxt end;
 
 fun user_proof after_qed some_prop =
diff -r 506f80a9afe8 -r 35f2b30593a8 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -774,7 +774,7 @@
     val loc_ctxt = thy'
       |> Locale.register_locale binding (extraTs, params)
           (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
-      |> TheoryTarget.init (SOME name)
+      |> Theory_Target.init (SOME name)
       |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
 
   in (name, loc_ctxt) end;
@@ -842,7 +842,7 @@
 fun gen_sublocale prep_expr intern raw_target expression thy =
   let
     val target = intern thy raw_target;
-    val target_ctxt = TheoryTarget.init (SOME target) thy;
+    val target_ctxt = Theory_Target.init (SOME target) thy;
     val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
     fun after_qed witss = ProofContext.theory
       (fold (fn ((dep, morph), wits) => Locale.add_dependency
diff -r 506f80a9afe8 -r 35f2b30593a8 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -390,7 +390,7 @@
 val _ =
   OuterSyntax.command "context" "enter local theory context" K.thy_decl
     (P.name --| P.begin >> (fn name =>
-      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name)));
+      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
 
 
 (* locales *)
@@ -452,7 +452,7 @@
   OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
    (P.multi_arity --| P.begin
      >> (fn arities => Toplevel.print o
-         Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
+         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
 
 val _ =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
@@ -470,7 +470,7 @@
       Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
       >> P.triple1) --| P.begin
    >> (fn operations => Toplevel.print o
-         Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
+         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
 
 
 (* code generation *)
diff -r 506f80a9afe8 -r 35f2b30593a8 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -19,7 +19,7 @@
   val overloading_cmd: (string * string * bool) list -> theory -> local_theory
 end;
 
-structure TheoryTarget: THEORY_TARGET =
+structure Theory_Target: THEORY_TARGET =
 struct
 
 (* context data *)
diff -r 506f80a9afe8 -r 35f2b30593a8 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 15:33:35 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 16:04:57 2009 +0100
@@ -103,7 +103,7 @@
 
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
-val loc_init = TheoryTarget.context;
+val loc_init = Theory_Target.context;
 val loc_exit = LocalTheory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
@@ -192,7 +192,7 @@
 
 (* print state *)
 
-val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
+val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
 
 fun print_state_context state =
   (case try node_of state of