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