--- 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 \
--- 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 {*
--- 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")
--- 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 {*
--- 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 \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" where
- "iso_tuple_update_accessor_cong_assist upd acc \<longleftrightarrow>
- (\<forall>f v. upd (\<lambda>x. f (acc v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
+ "iso_tuple_update_accessor_cong_assist upd ac \<longleftrightarrow>
+ (\<forall>f v. upd (\<lambda>x. f (ac v)) v = upd f v) \<and> (\<forall>v. upd id v = v)"
definition
iso_tuple_update_accessor_eq_assist ::
"(('b \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'a)) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool" where
- "iso_tuple_update_accessor_eq_assist upd acc v f v' x \<longleftrightarrow>
- upd f v = v' \<and> acc v = x \<and> iso_tuple_update_accessor_cong_assist upd acc"
+ "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<longleftrightarrow>
+ upd f v = v' \<and> ac v = x \<and> 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: "\<And>v. v' = v \<Longrightarrow> f v = f' v"
shows "upd f r = upd f' r'"
using uac r v [symmetric]
- apply (subgoal_tac "upd (\<lambda>x. f (acc r')) r' = upd (\<lambda>x. f' (acc r')) r'")
+ apply (subgoal_tac "upd (\<lambda>x. f (ac r')) r' = upd (\<lambda>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 \<Longrightarrow>
- r = r' \<Longrightarrow> acc r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
+ "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
+ r = r' \<Longrightarrow> ac r' = v' \<Longrightarrow> (\<And>v. v = v' \<Longrightarrow> f v = f' v) \<Longrightarrow>
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 \<Longrightarrow> upd id = id"
+ "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow> 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 \<circ> 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 \<Longrightarrow>
- iso_tuple_update_accessor_cong_assist upd acc"
+ "iso_tuple_update_accessor_cong_assist upd ac \<Longrightarrow>
+ 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 \<Longrightarrow> acc v = x"
+ "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> 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 \<Longrightarrow> upd f v = v'"
+ "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow> 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 \<Longrightarrow>
- iso_tuple_update_accessor_eq_assist upd acc v f v' x"
+ "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
+ 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 \<Longrightarrow>
- iso_tuple_update_accessor_cong_assist upd acc"
+ "iso_tuple_update_accessor_eq_assist upd ac v f v' x \<Longrightarrow>
+ 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
--- 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;
--- 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 =
--- 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);
--- 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;
--- 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);
--- 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);
--- 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
--- 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;
--- 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 =
--- 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
--- 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;
--- 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;
--- 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
--- 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);
--- 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);