modernized structure Theory_Target;
authorwenzelm
Tue Nov 10 16:04:57 2009 +0100 (2009-11-10)
changeset 3355335f2b30593a8
parent 33552 506f80a9afe8
child 33554 4601372337e4
modernized structure Theory_Target;
src/HOL/Code_Evaluation.thy
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/primrec.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/typecopy.ML
src/HOL/Typerep.thy
src/HOLCF/Tools/pcpodef.ML
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/theory_target.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/HOL/Code_Evaluation.thy	Tue Nov 10 15:33:35 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Nov 10 16:04:57 2009 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4          o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     1.5      in
     1.6        thy
     1.7 -      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
     1.8 +      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
     1.9        |> `(fn lthy => Syntax.check_term lthy eq)
    1.10        |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    1.11        |> snd
     2.1 --- a/src/HOL/Statespace/state_space.ML	Tue Nov 10 15:33:35 2009 +0100
     2.2 +++ b/src/HOL/Statespace/state_space.ML	Tue Nov 10 16:04:57 2009 +0100
     2.3 @@ -349,7 +349,7 @@
     2.4  
     2.5  fun add_declaration name decl thy =
     2.6    thy
     2.7 -  |> TheoryTarget.init name
     2.8 +  |> Theory_Target.init name
     2.9    |> (fn lthy => LocalTheory.declaration false (decl lthy) lthy)
    2.10    |> LocalTheory.exit_global;
    2.11  
     3.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 15:33:35 2009 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Nov 10 16:04:57 2009 +0100
     3.3 @@ -411,7 +411,7 @@
     3.4          #> fold_rev Code.add_eqn thms);
     3.5    in
     3.6      thy
     3.7 -    |> TheoryTarget.instantiation (dtcos, vs, [HOLogic.class_eq])
     3.8 +    |> Theory_Target.instantiation (dtcos, vs, [HOLogic.class_eq])
     3.9      |> fold_map add_def dtcos
    3.10      |-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm)
    3.11           (fn _ => fn def_thms => tac def_thms) def_thms)
     4.1 --- a/src/HOL/Tools/Function/size.ML	Tue Nov 10 15:33:35 2009 +0100
     4.2 +++ b/src/HOL/Tools/Function/size.ML	Tue Nov 10 16:04:57 2009 +0100
     4.3 @@ -144,7 +144,7 @@
     4.4        |> PureThy.add_defs false
     4.5          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
     4.6             (map Binding.name def_names ~~ (size_fns ~~ rec_combs1)))
     4.7 -      ||> TheoryTarget.instantiation
     4.8 +      ||> Theory_Target.instantiation
     4.9             (map (#1 o snd) descr', map dest_TFree paramTs, [HOLogic.class_size])
    4.10        ||>> fold_map define_overloaded
    4.11          (def_names' ~~ map Logic.mk_equals (overloaded_size_fns ~~ map (app fs') rec_combs1))
     5.1 --- a/src/HOL/Tools/inductive.ML	Tue Nov 10 15:33:35 2009 +0100
     5.2 +++ b/src/HOL/Tools/inductive.ML	Tue Nov 10 16:04:57 2009 +0100
     5.3 @@ -895,7 +895,7 @@
     5.4    let
     5.5      val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     5.6      val ctxt' = thy
     5.7 -      |> TheoryTarget.init NONE
     5.8 +      |> Theory_Target.init NONE
     5.9        |> LocalTheory.set_group group
    5.10        |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
    5.11        |> LocalTheory.exit;
     6.1 --- a/src/HOL/Tools/primrec.ML	Tue Nov 10 15:33:35 2009 +0100
     6.2 +++ b/src/HOL/Tools/primrec.ML	Tue Nov 10 16:04:57 2009 +0100
     6.3 @@ -293,14 +293,14 @@
     6.4  
     6.5  fun add_primrec_global fixes specs thy =
     6.6    let
     6.7 -    val lthy = TheoryTarget.init NONE thy;
     6.8 +    val lthy = Theory_Target.init NONE thy;
     6.9      val (simps, lthy') = add_primrec fixes specs lthy;
    6.10      val simps' = ProofContext.export lthy' lthy simps;
    6.11    in (simps', LocalTheory.exit_global lthy') end;
    6.12  
    6.13  fun add_primrec_overloaded ops fixes specs thy =
    6.14    let
    6.15 -    val lthy = TheoryTarget.overloading ops thy;
    6.16 +    val lthy = Theory_Target.overloading ops thy;
    6.17      val (simps, lthy') = add_primrec fixes specs lthy;
    6.18      val simps' = ProofContext.export lthy' lthy simps;
    6.19    in (simps', LocalTheory.exit_global lthy') end;
     7.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 15:33:35 2009 +0100
     7.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Nov 10 16:04:57 2009 +0100
     7.3 @@ -82,7 +82,7 @@
     7.4      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     7.5    in   
     7.6      thy
     7.7 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
     7.8 +    |> Theory_Target.instantiation ([tyco], vs, @{sort random})
     7.9      |> `(fn lthy => Syntax.check_term lthy eq)
    7.10      |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
    7.11      |> snd
    7.12 @@ -300,7 +300,7 @@
    7.13        (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts;
    7.14    in
    7.15      thy
    7.16 -    |> TheoryTarget.instantiation (tycos, vs, @{sort random})
    7.17 +    |> Theory_Target.instantiation (tycos, vs, @{sort random})
    7.18      |> random_aux_specification prfx random_auxN auxs_eqs
    7.19      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
    7.20      |-> (fn random_defs' => fold_map (fn random_def =>
     8.1 --- a/src/HOL/Tools/typecopy.ML	Tue Nov 10 15:33:35 2009 +0100
     8.2 +++ b/src/HOL/Tools/typecopy.ML	Tue Nov 10 16:04:57 2009 +0100
     8.3 @@ -113,7 +113,7 @@
     8.4      thy
     8.5      |> Code.add_datatype [constr]
     8.6      |> Code.add_eqn proj_eq
     8.7 -    |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq])
     8.8 +    |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
     8.9      |> `(fn lthy => Syntax.check_term lthy eq)
    8.10      |-> (fn eq => Specification.definition
    8.11           (NONE, (Attrib.empty_binding, eq)))
     9.1 --- a/src/HOL/Typerep.thy	Tue Nov 10 15:33:35 2009 +0100
     9.2 +++ b/src/HOL/Typerep.thy	Tue Nov 10 16:04:57 2009 +0100
     9.3 @@ -50,7 +50,7 @@
     9.4      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     9.5    in
     9.6      thy
     9.7 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
     9.8 +    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     9.9      |> `(fn lthy => Syntax.check_term lthy eq)
    9.10      |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    9.11      |> snd
    10.1 --- a/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 15:33:35 2009 +0100
    10.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Tue Nov 10 16:04:57 2009 +0100
    10.3 @@ -75,7 +75,7 @@
    10.4          val ((_, {type_definition, set_def, ...}), thy2) = thy1
    10.5            |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
    10.6          val lthy3 = thy2
    10.7 -          |> TheoryTarget.instantiation ([full_tname], lhs_tfrees, @{sort po});
    10.8 +          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
    10.9          val below_def' = Syntax.check_term lthy3 below_def;
   10.10          val ((_, (_, below_definition')), lthy4) = lthy3
   10.11            |> Specification.definition (NONE,
    11.1 --- a/src/Pure/Isar/class.ML	Tue Nov 10 15:33:35 2009 +0100
    11.2 +++ b/src/Pure/Isar/class.ML	Tue Nov 10 16:04:57 2009 +0100
    11.3 @@ -290,7 +290,7 @@
    11.4         Locale.add_registration (class, base_morph $> eq_morph) NONE export_morph
    11.5           (*FIXME should not modify base_morph, although admissible*)
    11.6      #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
    11.7 -    |> TheoryTarget.init (SOME class)
    11.8 +    |> Theory_Target.init (SOME class)
    11.9      |> pair class
   11.10    end;
   11.11  
   11.12 @@ -310,7 +310,7 @@
   11.13    let
   11.14      val thy = ProofContext.theory_of lthy;
   11.15      val proto_sup = prep_class thy raw_sup;
   11.16 -    val proto_sub = case TheoryTarget.peek lthy
   11.17 +    val proto_sub = case Theory_Target.peek lthy
   11.18       of {is_class = false, ...} => error "Not in a class context"
   11.19        | {target, ...} => target;
   11.20      val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   11.21 @@ -323,7 +323,7 @@
   11.22      fun after_qed some_wit =
   11.23        ProofContext.theory (register_subclass (sub, sup)
   11.24          some_dep_morph some_wit export)
   11.25 -      #> ProofContext.theory_of #> TheoryTarget.init (SOME sub);
   11.26 +      #> ProofContext.theory_of #> Theory_Target.init (SOME sub);
   11.27    in do_proof after_qed some_prop goal_ctxt end;
   11.28  
   11.29  fun user_proof after_qed some_prop =
    12.1 --- a/src/Pure/Isar/expression.ML	Tue Nov 10 15:33:35 2009 +0100
    12.2 +++ b/src/Pure/Isar/expression.ML	Tue Nov 10 16:04:57 2009 +0100
    12.3 @@ -774,7 +774,7 @@
    12.4      val loc_ctxt = thy'
    12.5        |> Locale.register_locale binding (extraTs, params)
    12.6            (asm, rev defs) (a_intro, b_intro) axioms ([], []) (rev notes) (rev deps')
    12.7 -      |> TheoryTarget.init (SOME name)
    12.8 +      |> Theory_Target.init (SOME name)
    12.9        |> fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes';
   12.10  
   12.11    in (name, loc_ctxt) end;
   12.12 @@ -842,7 +842,7 @@
   12.13  fun gen_sublocale prep_expr intern raw_target expression thy =
   12.14    let
   12.15      val target = intern thy raw_target;
   12.16 -    val target_ctxt = TheoryTarget.init (SOME target) thy;
   12.17 +    val target_ctxt = Theory_Target.init (SOME target) thy;
   12.18      val ((propss, deps, export), goal_ctxt) = prep_expr expression target_ctxt;
   12.19      fun after_qed witss = ProofContext.theory
   12.20        (fold (fn ((dep, morph), wits) => Locale.add_dependency
    13.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Nov 10 15:33:35 2009 +0100
    13.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 10 16:04:57 2009 +0100
    13.3 @@ -390,7 +390,7 @@
    13.4  val _ =
    13.5    OuterSyntax.command "context" "enter local theory context" K.thy_decl
    13.6      (P.name --| P.begin >> (fn name =>
    13.7 -      Toplevel.print o Toplevel.begin_local_theory true (TheoryTarget.context name)));
    13.8 +      Toplevel.print o Toplevel.begin_local_theory true (Theory_Target.context name)));
    13.9  
   13.10  
   13.11  (* locales *)
   13.12 @@ -452,7 +452,7 @@
   13.13    OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl
   13.14     (P.multi_arity --| P.begin
   13.15       >> (fn arities => Toplevel.print o
   13.16 -         Toplevel.begin_local_theory true (TheoryTarget.instantiation_cmd arities)));
   13.17 +         Toplevel.begin_local_theory true (Theory_Target.instantiation_cmd arities)));
   13.18  
   13.19  val _ =
   13.20    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
   13.21 @@ -470,7 +470,7 @@
   13.22        Scan.optional (P.$$$ "(" |-- (P.$$$ "unchecked" >> K false) --| P.$$$ ")") true
   13.23        >> P.triple1) --| P.begin
   13.24     >> (fn operations => Toplevel.print o
   13.25 -         Toplevel.begin_local_theory true (TheoryTarget.overloading_cmd operations)));
   13.26 +         Toplevel.begin_local_theory true (Theory_Target.overloading_cmd operations)));
   13.27  
   13.28  
   13.29  (* code generation *)
    14.1 --- a/src/Pure/Isar/theory_target.ML	Tue Nov 10 15:33:35 2009 +0100
    14.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Nov 10 16:04:57 2009 +0100
    14.3 @@ -19,7 +19,7 @@
    14.4    val overloading_cmd: (string * string * bool) list -> theory -> local_theory
    14.5  end;
    14.6  
    14.7 -structure TheoryTarget: THEORY_TARGET =
    14.8 +structure Theory_Target: THEORY_TARGET =
    14.9  struct
   14.10  
   14.11  (* context data *)
    15.1 --- a/src/Pure/Isar/toplevel.ML	Tue Nov 10 15:33:35 2009 +0100
    15.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Nov 10 16:04:57 2009 +0100
    15.3 @@ -103,7 +103,7 @@
    15.4  
    15.5  type generic_theory = Context.generic;    (*theory or local_theory*)
    15.6  
    15.7 -val loc_init = TheoryTarget.context;
    15.8 +val loc_init = Theory_Target.context;
    15.9  val loc_exit = LocalTheory.exit_global;
   15.10  
   15.11  fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   15.12 @@ -192,7 +192,7 @@
   15.13  
   15.14  (* print state *)
   15.15  
   15.16 -val pretty_context = LocalTheory.pretty o Context.cases (TheoryTarget.init NONE) I;
   15.17 +val pretty_context = LocalTheory.pretty o Context.cases (Theory_Target.init NONE) I;
   15.18  
   15.19  fun print_state_context state =
   15.20    (case try node_of state of