# HG changeset patch # User haftmann # Date 1281635276 -7200 # Node ID 3cb4280c4cf141daaf1fcfad08c6516c03106406 # Parent f31678522745e35c58f575b273c1a9d2004f9566# Parent 2d6dc3f25686b8b37184f78b501ef09d7f02fe6a merged diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/IsaMakefile Thu Aug 12 19:47:56 2010 +0200 @@ -207,14 +207,12 @@ Tools/old_primrec.ML \ Tools/primrec.ML \ Tools/prop_logic.ML \ - Tools/record.ML \ Tools/refute.ML \ Tools/refute_isar.ML \ Tools/rewrite_hol_proof.ML \ Tools/sat_funcs.ML \ Tools/sat_solver.ML \ Tools/split_rule.ML \ - Tools/typecopy.ML \ Tools/typedef_codegen.ML \ Tools/typedef.ML \ Transitive_Closure.thy \ @@ -305,6 +303,7 @@ Tools/Predicate_Compile/predicate_compile_specialisation.ML \ Tools/Predicate_Compile/predicate_compile_pred.ML \ Tools/quickcheck_generators.ML \ + Tools/quickcheck_record.ML \ Tools/Qelim/cooper.ML \ Tools/Qelim/cooper_procedure.ML \ Tools/Qelim/qelim.ML \ @@ -314,6 +313,7 @@ Tools/Quotient/quotient_term.ML \ Tools/Quotient/quotient_typ.ML \ Tools/recdef.ML \ + Tools/record.ML \ Tools/semiring_normalizer.ML \ Tools/Sledgehammer/clausifier.ML \ Tools/Sledgehammer/meson_tactic.ML \ @@ -343,6 +343,7 @@ Tools/string_code.ML \ Tools/string_syntax.ML \ Tools/transfer.ML \ + Tools/typecopy.ML \ Tools/TFL/casesplit.ML \ Tools/TFL/dcterm.ML \ Tools/TFL/post.ML \ diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Main.thy --- a/src/HOL/Main.thy Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Main.thy Thu Aug 12 19:47:56 2010 +0200 @@ -1,7 +1,7 @@ header {* Main HOL *} theory Main -imports Plain Predicate_Compile Nitpick SMT +imports Plain Record Predicate_Compile Nitpick SMT begin text {* diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Nitpick.thy Thu Aug 12 19:47:56 2010 +0200 @@ -8,7 +8,7 @@ header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} theory Nitpick -imports Map Quotient SAT +imports Map Quotient SAT Record uses ("Tools/Nitpick/kodkod.ML") ("Tools/Nitpick/kodkod_sat.ML") ("Tools/Nitpick/nitpick_util.ML") diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Plain.thy --- a/src/HOL/Plain.thy Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Plain.thy Thu Aug 12 19:47:56 2010 +0200 @@ -1,7 +1,7 @@ header {* Plain HOL *} theory Plain -imports Datatype Record FunDef Extraction +imports Datatype FunDef Extraction begin text {* diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Record.thy --- a/src/HOL/Record.thy Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Record.thy Thu Aug 12 19:47:56 2010 +0200 @@ -9,8 +9,8 @@ header {* Extensible records with structural subtyping *} theory Record -imports Datatype -uses ("Tools/record.ML") +imports Plain Quickcheck +uses ("Tools/typecopy.ML") ("Tools/record.ML") ("Tools/quickcheck_record.ML") begin subsection {* Introduction *} @@ -123,67 +123,67 @@ definition iso_tuple_update_accessor_cong_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ bool" where - "iso_tuple_update_accessor_cong_assist upd acc \ - (\f v. upd (\x. f (acc v)) v = upd f v) \ (\v. upd id v = v)" + "iso_tuple_update_accessor_cong_assist upd ac \ + (\f v. upd (\x. f (ac v)) v = upd f v) \ (\v. upd id v = v)" definition iso_tuple_update_accessor_eq_assist :: "(('b \ 'b) \ ('a \ 'a)) \ ('a \ 'b) \ 'a \ ('b \ 'b) \ 'a \ 'b \ bool" where - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - upd f v = v' \ acc v = x \ iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + upd f v = v' \ ac v = x \ iso_tuple_update_accessor_cong_assist upd ac" lemma update_accessor_congruence_foldE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and r: "r = r'" and v: "acc r' = v'" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and r: "r = r'" and v: "ac r' = v'" and f: "\v. v' = v \ f v = f' v" shows "upd f r = upd f' r'" using uac r v [symmetric] - apply (subgoal_tac "upd (\x. f (acc r')) r' = upd (\x. f' (acc r')) r'") + apply (subgoal_tac "upd (\x. f (ac r')) r' = upd (\x. f' (ac r')) r'") apply (simp add: iso_tuple_update_accessor_cong_assist_def) apply (simp add: f) done lemma update_accessor_congruence_unfoldE: - "iso_tuple_update_accessor_cong_assist upd acc \ - r = r' \ acc r' = v' \ (\v. v = v' \ f v = f' v) \ + "iso_tuple_update_accessor_cong_assist upd ac \ + r = r' \ ac r' = v' \ (\v. v = v' \ f v = f' v) \ upd f r = upd f' r'" apply (erule(2) update_accessor_congruence_foldE) apply simp done lemma iso_tuple_update_accessor_cong_assist_id: - "iso_tuple_update_accessor_cong_assist upd acc \ upd id = id" + "iso_tuple_update_accessor_cong_assist upd ac \ upd id = id" by rule (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_noopE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd f x = x" using uac - by (simp add: acc iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] + by (simp add: ac iso_tuple_update_accessor_cong_assist_id [OF uac, unfolded id_def] cong: update_accessor_congruence_unfoldE [OF uac]) lemma update_accessor_noop_compE: - assumes uac: "iso_tuple_update_accessor_cong_assist upd acc" - and acc: "f (acc x) = acc x" + assumes uac: "iso_tuple_update_accessor_cong_assist upd ac" + and ac: "f (ac x) = ac x" shows "upd (g \ f) x = upd g x" - by (simp add: acc cong: update_accessor_congruence_unfoldE[OF uac]) + by (simp add: ac cong: update_accessor_congruence_unfoldE[OF uac]) lemma update_accessor_cong_assist_idI: "iso_tuple_update_accessor_cong_assist id id" by (simp add: iso_tuple_update_accessor_cong_assist_def) lemma update_accessor_cong_assist_triv: - "iso_tuple_update_accessor_cong_assist upd acc \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_cong_assist upd ac \ + iso_tuple_update_accessor_cong_assist upd ac" by assumption lemma update_accessor_accessor_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ acc v = x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ ac v = x" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma update_accessor_updator_eqE: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ upd f v = v'" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ upd f v = v'" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_update_accessor_eq_assist_idI: @@ -191,13 +191,13 @@ by (simp add: iso_tuple_update_accessor_eq_assist_def update_accessor_cong_assist_idI) lemma iso_tuple_update_accessor_eq_assist_triv: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_eq_assist upd acc v f v' x" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_eq_assist upd ac v f v' x" by assumption lemma iso_tuple_update_accessor_cong_from_eq: - "iso_tuple_update_accessor_eq_assist upd acc v f v' x \ - iso_tuple_update_accessor_cong_assist upd acc" + "iso_tuple_update_accessor_eq_assist upd ac v f v' x \ + iso_tuple_update_accessor_cong_assist upd ac" by (simp add: iso_tuple_update_accessor_eq_assist_def) lemma iso_tuple_surjective_proof_assistI: @@ -452,8 +452,9 @@ subsection {* Record package *} -use "Tools/record.ML" -setup Record.setup +use "Tools/typecopy.ML" setup Typecopy.setup +use "Tools/record.ML" setup Record.setup +use "Tools/quickcheck_record.ML" setup Quickcheck_Record.setup hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd iso_tuple_fst_update iso_tuple_snd_update iso_tuple_cons diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Statespace/state_space.ML Thu Aug 12 19:47:56 2010 +0200 @@ -466,7 +466,7 @@ (suffix valuetypesN full_name,(("",false),Expression.Named []))],[]) fixestate |> ProofContext.theory_of |> fold interprete_parent parents - |> add_declaration (SOME full_name) (declare_declinfo components') + |> add_declaration full_name (declare_declinfo components') end; diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 12 19:47:56 2010 +0200 @@ -511,8 +511,6 @@ clearly inconsistent facts such as X = a | X = b, though it by no means guarantees soundness. *) -fun is_record_type T = not (null (Record.dest_recTs T)) - (* Unwanted equalities are those between a (bound or schematic) variable that does not properly occur in the second operand. *) fun too_general_eqterms (Var z) t = diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Tools/inductive.ML Thu Aug 12 19:47:56 2010 +0200 @@ -998,7 +998,7 @@ let val name = Sign.full_name thy (fst (fst (hd cnames_syn))); val ctxt' = thy - |> Named_Target.init NONE + |> Named_Target.theory_init |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd |> Local_Theory.exit; val info = #2 (the_inductive ctxt' name); diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Tools/primrec.ML --- a/src/HOL/Tools/primrec.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Tools/primrec.ML Thu Aug 12 19:47:56 2010 +0200 @@ -292,7 +292,7 @@ fun add_primrec_global fixes specs thy = let - val lthy = Named_Target.init NONE thy; + val lthy = Named_Target.theory_init 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; diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Tools/quickcheck_generators.ML Thu Aug 12 19:47:56 2010 +0200 @@ -10,7 +10,6 @@ val random_fun: typ -> typ -> ('a -> 'a -> bool) -> ('a -> term) -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed) -> seed -> (('a -> 'b) * (unit -> term)) * seed - val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> string -> term list -> local_theory -> local_theory val mk_random_aux_eqs: theory -> Datatype.descr -> (string * sort) list -> string list -> string list * string list -> typ list * typ list @@ -65,53 +64,10 @@ in ((random_fun', term_fun'), seed''') end; -(** type copies **) - -fun mk_random_typecopy tyco vs constr T' thy = - let - val mk_const = curry (Sign.mk_const thy); - val Ts = map TFree vs; - val T = Type (tyco, Ts); - val Tm = termifyT T; - val Tm' = termifyT T'; - val v = "x"; - val t_v = Free (v, Tm'); - val t_constr = Const (constr, T' --> T); - val lhs = HOLogic.mk_random T size; - val rhs = HOLogic.mk_ST [((HOLogic.mk_random T' size, @{typ Random.seed}), SOME (v, Tm'))] - (HOLogic.mk_return Tm @{typ Random.seed} - (mk_const "Code_Evaluation.valapp" [T', T] - $ HOLogic.mk_prod (t_constr, Abs ("u", @{typ unit}, HOLogic.reflect_term t_constr)) $ t_v)) - @{typ Random.seed} (SOME Tm, @{typ Random.seed}); - val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); - in - thy - |> 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 - |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) - end; - -fun ensure_random_typecopy tyco thy = - let - val SOME { vs = raw_vs, constr, typ = raw_T, ... } = - Typecopy.get_info thy tyco; - val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)); - val T = map_atyps (fn TFree (v, sort) => - TFree (v, constrain sort @{sort random})) raw_T; - val vs' = Term.add_tfreesT T []; - val vs = map (fn (v, sort) => - (v, the_default (constrain sort @{sort typerep}) (AList.lookup (op =) vs' v))) raw_vs; - val can_inst = Sign.of_sort thy (T, @{sort random}); - in if can_inst then mk_random_typecopy tyco vs constr T thy else thy end; - - (** datatypes **) (* definitional scheme for random instances on datatypes *) -(*FIXME avoid this low-level proving*) local fun dest_ctyp_nth k cT = nth (Thm.dest_ctyp cT) k; @@ -450,8 +406,8 @@ (** setup **) -val setup = Typecopy.interpretation ensure_random_typecopy - #> Datatype.interpretation ensure_random_datatype +val setup = + Datatype.interpretation ensure_random_datatype #> Code_Target.extend_target (target, (Code_Eval.target, K I)) #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of); diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Tools/typedef.ML Thu Aug 12 19:47:56 2010 +0200 @@ -268,7 +268,7 @@ in typedef_result inhabited lthy' end; fun add_typedef_global def opt_name typ set opt_morphs tac = - Named_Target.init NONE + Named_Target.theory_init #> add_typedef def opt_name typ set opt_morphs tac #> Local_Theory.exit_result_global (apsnd o transform_info); diff -r f31678522745 -r 3cb4280c4cf1 src/HOL/Typedef.thy --- a/src/HOL/Typedef.thy Thu Aug 12 20:11:13 2010 +0800 +++ b/src/HOL/Typedef.thy Thu Aug 12 19:47:56 2010 +0200 @@ -8,7 +8,6 @@ imports Set uses ("Tools/typedef.ML") - ("Tools/typecopy.ML") ("Tools/typedef_codegen.ML") begin @@ -116,7 +115,6 @@ end use "Tools/typedef.ML" setup Typedef.setup -use "Tools/typecopy.ML" setup Typecopy.setup use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup end diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/class.ML Thu Aug 12 19:47:56 2010 +0200 @@ -17,7 +17,7 @@ val print_classes: theory -> unit val init: class -> theory -> Proof.context val begin: class list -> sort -> Proof.context -> Proof.context - val declare: class -> (binding * mixfix) * (term list * term) -> theory -> theory + val const: class -> (binding * mixfix) * (term list * term) -> theory -> theory val abbrev: class -> Syntax.mode -> (binding * mixfix) * term -> theory -> theory val refresh_syntax: class -> Proof.context -> Proof.context val redeclare_operations: theory -> sort -> Proof.context -> Proof.context @@ -312,7 +312,7 @@ val class_prefix = Logic.const_of_class o Long_Name.base_name; -fun declare class ((c, mx), (type_params, dict)) thy = +fun const class ((c, mx), (type_params, dict)) thy = let val morph = morphism thy class; val b = Morphism.binding morph c; diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/class_declaration.ML Thu Aug 12 19:47:56 2010 +0200 @@ -290,7 +290,7 @@ Context.theory_map (Locale.add_registration (class, base_morph) (Option.map (rpair true) eq_morph) export_morph) #> Class.register class sups params base_sort base_morph export_morph axiom assm_intro of_class)) - |> Named_Target.init (SOME class) + |> Named_Target.init class |> pair class end; @@ -311,8 +311,8 @@ val thy = ProofContext.theory_of lthy; val proto_sup = prep_class thy raw_sup; val proto_sub = case Named_Target.peek lthy - of {is_class = false, ...} => error "Not in a class context" - | {target, ...} => target; + of SOME {target, is_class = true, ...} => target + | _ => error "Not in a class target"; val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); val expr = ([(sup, (("", false), Expression.Positional []))], []); @@ -323,7 +323,7 @@ fun after_qed some_wit = ProofContext.theory (Class.register_subclass (sub, sup) some_dep_morph some_wit export) - #> ProofContext.theory_of #> Named_Target.init (SOME sub); + #> ProofContext.theory_of #> Named_Target.init sub; in do_proof after_qed some_prop goal_ctxt end; fun user_proof after_qed some_prop = diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/expression.ML Thu Aug 12 19:47:56 2010 +0200 @@ -775,7 +775,7 @@ val loc_ctxt = thy' |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms [] (rev notes) (rev deps') - |> Named_Target.init (SOME name) + |> Named_Target.init name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; @@ -870,7 +870,7 @@ fun gen_sublocale prep_expr intern raw_target expression thy = let val target = intern thy raw_target; - val target_ctxt = Named_Target.init (SOME target) thy; + val target_ctxt = Named_Target.init 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 f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/named_target.ML --- a/src/Pure/Isar/named_target.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/named_target.ML Thu Aug 12 19:47:56 2010 +0200 @@ -7,9 +7,11 @@ signature NAMED_TARGET = sig - val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} - val init: string option -> theory -> local_theory + val init: string -> theory -> local_theory + val theory_init: theory -> local_theory + val reinit: local_theory -> local_theory -> local_theory val context_cmd: xstring -> theory -> local_theory + val peek: local_theory -> {target: string, is_locale: bool, is_class: bool} option end; structure Named_Target: NAMED_TARGET = @@ -24,19 +26,19 @@ val global_target = Target {target = "", is_locale = false, is_class = false}; -fun named_target _ NONE = global_target - | named_target thy (SOME locale) = +fun named_target _ "" = global_target + | named_target thy locale = if Locale.defined thy locale then Target {target = locale, is_locale = true, is_class = Class.is_class thy locale} else error ("No such locale: " ^ quote locale); structure Data = Proof_Data ( - type T = target; - fun init _ = global_target; + type T = target option; + fun init _ = NONE; ); -val peek = (fn Target args => args) o Data.get; +val peek = Option.map (fn Target args => args) o Data.get; (* generic declarations *) @@ -102,7 +104,7 @@ (((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, NoSyn), lhs) - #> class_target ta (Class.declare target ((b, mx), (type_params, lhs))) + #> class_target ta (Class.const target ((b, mx), (type_params, lhs))) #> pair (lhs, def)) fun target_foundation (ta as Target {target, is_locale, is_class, ...}) = @@ -186,7 +188,7 @@ fun init_target (ta as Target {target, ...}) thy = thy |> init_context ta - |> Data.put ta + |> Data.put (SOME ta) |> Local_Theory.init NONE (Long_Name.base_name target) {define = Generic_Target.define (target_foundation ta), notes = Generic_Target.notes (target_notes ta), @@ -202,8 +204,14 @@ fun init target thy = init_target (named_target thy target) thy; -fun context_cmd "-" thy = init NONE thy - | context_cmd target thy = init (SOME (Locale.intern thy target)) thy; +fun reinit lthy = case peek lthy + of SOME {target, ...} => init target o Local_Theory.exit_global + | NONE => error "Not in a named target"; + +val theory_init = init_target global_target; + +fun context_cmd "-" thy = init "" thy + | context_cmd target thy = init (Locale.intern thy target) thy; end; diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/specification.ML Thu Aug 12 19:47:56 2010 +0200 @@ -185,7 +185,7 @@ (*facts*) val (facts, facts_lthy) = axioms_thy - |> Named_Target.init NONE + |> Named_Target.theory_init |> Spec_Rules.add Spec_Rules.Unknown (consts, maps (maps #1 o #2) axioms) |> Local_Theory.notes axioms; diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/toplevel.ML Thu Aug 12 19:47:56 2010 +0200 @@ -107,14 +107,11 @@ fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy | loc_begin NONE (Context.Proof lthy) = lthy - | loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); + | loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit | loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore - | loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => let - val target_name = #target (Named_Target.peek lthy); - val target = if target_name = "" then NONE else SOME target_name; - in Context.Proof (Named_Target.init target (loc_exit lthy')) end; + | loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; (* datatype node *) @@ -193,7 +190,7 @@ (* print state *) -val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.init NONE) I; +val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; fun print_state_context state = (case try node_of state of diff -r f31678522745 -r 3cb4280c4cf1 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Pure/Isar/typedecl.ML Thu Aug 12 19:47:56 2010 +0200 @@ -75,7 +75,7 @@ end; fun typedecl_global decl = - Named_Target.init NONE + Named_Target.theory_init #> typedecl decl #> Local_Theory.exit_result_global Morphism.typ; @@ -115,7 +115,7 @@ end; fun abbrev_global decl rhs = - Named_Target.init NONE + Named_Target.theory_init #> abbrev decl rhs #> Local_Theory.exit_result_global (K I); diff -r f31678522745 -r 3cb4280c4cf1 src/Tools/quickcheck.ML --- a/src/Tools/quickcheck.ML Thu Aug 12 20:11:13 2010 +0800 +++ b/src/Tools/quickcheck.ML Thu Aug 12 19:47:56 2010 +0200 @@ -219,9 +219,10 @@ | strip t = t; val {goal = st, ...} = Proof.raw_goal state; val (gi, frees) = Logic.goal_params (prop_of st) i; - val some_locale = case (#target o Named_Target.peek) lthy - of "" => NONE - | locale => SOME locale; + val some_locale = case (Option.map #target o Named_Target.peek) lthy + of NONE => NONE + | SOME "" => NONE + | SOME locale => SOME locale; val assms = if no_assms then [] else case some_locale of NONE => Assumption.all_assms_of lthy | SOME locale => Assumption.local_assms_of lthy (Locale.init locale thy);