--- a/src/Pure/Isar/locale.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/Isar/locale.ML Wed Nov 29 23:33:09 2006 +0100
@@ -1809,7 +1809,7 @@
val (ctxt, (_, facts)) = activate_facts true (K I)
(ProofContext.init pred_thy, axiomify predicate_axioms elemss');
val view_ctxt = Assumption.add_view thy_ctxt predicate_statement ctxt;
- val export = Drule.local_standard o singleton (ProofContext.export view_ctxt thy_ctxt);
+ val export = singleton (ProofContext.export_standard view_ctxt thy_ctxt);
val facts' = facts |> map (fn (a, ths) => ((a, []), [(map export ths, [])]));
val elems' = maps #2 (filter (equal "" o #1 o #1) elemss');
val elems'' = map_filter (fn (Fixes _) => NONE | e => SOME e) elems';
--- a/src/Pure/Isar/proof_context.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Nov 29 23:33:09 2006 +0100
@@ -70,6 +70,8 @@
val read_const: Proof.context -> string -> term
val goal_export: Proof.context -> Proof.context -> thm list -> thm list
val export: Proof.context -> Proof.context -> thm list -> thm list
+ val export_standard: Proof.context -> Proof.context -> thm list -> thm list
+ val standard: Proof.context -> thm list -> thm list
val export_morphism: Proof.context -> Proof.context -> morphism
val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
@@ -570,7 +572,9 @@
-(** export results **)
+(** export theorems **)
+
+(* rules *)
fun common_export is_goal inner outer =
map (Assumption.export is_goal inner outer) #>
@@ -579,6 +583,14 @@
val goal_export = common_export true;
val export = common_export false;
+fun export_standard inner outer =
+ export inner outer #> map Drule.local_standard;
+
+fun standard ctxt = export_standard ctxt ctxt;
+
+
+(* morphisms *)
+
fun export_morphism inner outer =
Assumption.export_morphism inner outer $>
Variable.export_morphism inner outer;
--- a/src/Pure/drule.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/drule.ML Wed Nov 29 23:33:09 2006 +0100
@@ -38,7 +38,6 @@
val implies_elim_list: thm -> thm list -> thm
val implies_intr_list: cterm list -> thm -> thm
val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
- val zero_var_indexes_list: thm list -> thm list
val zero_var_indexes: thm -> thm
val implies_intr_hyps: thm -> thm
val standard: thm -> thm
@@ -100,7 +99,6 @@
val add_used: thm -> string list -> string list
val flexflex_unique: thm -> thm
val close_derivation: thm -> thm
- val local_standard': thm -> thm
val local_standard: thm -> thm
val store_thm: bstring -> thm -> thm
val store_standard_thm: bstring -> thm -> thm
@@ -399,17 +397,14 @@
fun implies_elim_list impth ths = Library.foldl (uncurry implies_elim) (impth,ths);
(*Reset Var indexes to zero, renaming to preserve distinctness*)
-fun zero_var_indexes_list [] = []
- | zero_var_indexes_list ths =
- let
- val thy = Theory.merge_list (map Thm.theory_of_thm ths);
- val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
- val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
- val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
- val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
- in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
-
-val zero_var_indexes = singleton zero_var_indexes_list;
+fun zero_var_indexes th =
+ let
+ val thy = Thm.theory_of_thm th;
+ val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
+ val (instT, inst) = TermSubst.zero_var_indexes_inst (Thm.full_prop_of th);
+ val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
+ val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
+ in Thm.adjust_maxidx_thm ~1 (Thm.instantiate (cinstT, cinst) th) end;
(** Standard form of object-rule: no hypotheses, flexflex constraints,
@@ -441,20 +436,17 @@
#> Thm.strip_shyps
#> zero_var_indexes
#> Thm.varifyT
- #> Thm.compress); (* FIXME !? *)
+ #> Thm.compress);
val standard =
- flexflex_unique (* FIXME !? *)
+ flexflex_unique
#> standard'
#> close_derivation;
-val local_standard' =
+val local_standard =
flexflex_unique
#> Thm.strip_shyps
- #> zero_var_indexes;
-
-val local_standard =
- local_standard'
+ #> zero_var_indexes
#> Thm.compress
#> close_derivation;
@@ -870,21 +862,11 @@
else cterm_fun (Pattern.rewrite_term (Thm.theory_of_cterm ct) [norm_hhf_prop] []) ct;
-(* var indexes *)
-
-fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
-
-fun incr_indexes2 th1 th2 =
- Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
-
-fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
-fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
-
(*** Instantiate theorem th, reading instantiations in theory thy ****)
(*Version that normalizes the result: Thm.instantiate no longer does that*)
-fun instantiate instpair th = Thm.instantiate instpair th COMP_INCR asm_rl;
+fun instantiate instpair th = Thm.instantiate instpair th COMP asm_rl;
fun read_instantiate_sg' thy sinsts th =
let val ts = types_sorts th;
@@ -1070,6 +1052,17 @@
end;
+(* var indexes *)
+
+fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);
+
+fun incr_indexes2 th1 th2 =
+ Thm.incr_indexes (Int.max (Thm.maxidx_of th1, Thm.maxidx_of th2) + 1);
+
+fun th1 INCR_COMP th2 = incr_indexes th2 th1 COMP th2;
+fun th1 COMP_INCR th2 = th1 COMP incr_indexes th1 th2;
+
+
(** multi_resolve **)
--- a/src/Pure/pure_thy.ML Wed Nov 29 23:28:13 2006 +0100
+++ b/src/Pure/pure_thy.ML Wed Nov 29 23:33:09 2006 +0100
@@ -418,7 +418,10 @@
| smart_store name_thm (name, [thm]) =
fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
| smart_store name_thm (name, thms) =
- let val thy = Theory.merge_list (map Thm.theory_of_thm thms)
+ let
+ fun merge th thy = Theory.merge (thy, Thm.theory_of_thm th)
+ handle TERM (msg, _) => raise THM (msg, 0, [th]);
+ val thy = fold merge (tl thms) (Thm.theory_of_thm (hd thms));
in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
in