--- a/src/Pure/drule.ML Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Pure/drule.ML Sun Feb 07 19:33:34 2010 +0100
@@ -75,8 +75,8 @@
val beta_conv: cterm -> cterm -> cterm
val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option)
val flexflex_unique: thm -> thm
- val standard: thm -> thm
- val standard': thm -> thm
+ val export_without_context: thm -> thm
+ val export_without_context_open: thm -> thm
val get_def: theory -> xstring -> thm
val store_thm: binding -> thm -> thm
val store_standard_thm: binding -> thm -> thm
@@ -303,9 +303,9 @@
| _ => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
-(* legacy standard operations *)
+(* old-style export without context *)
-val standard' =
+val export_without_context_open =
implies_intr_hyps
#> forall_intr_frees
#> `Thm.maxidx_of
@@ -315,9 +315,9 @@
#> zero_var_indexes
#> Thm.varifyT);
-val standard =
+val export_without_context =
flexflex_unique
- #> standard'
+ #> export_without_context_open
#> Thm.close_derivation;
@@ -459,8 +459,8 @@
fun store_thm_open name th =
Context.>>> (Context.map_theory_result (PureThy.store_thm_open (name, th)));
-fun store_standard_thm name th = store_thm name (standard th);
-fun store_standard_thm_open name thm = store_thm_open name (standard' thm);
+fun store_standard_thm name th = store_thm name (export_without_context th);
+fun store_standard_thm_open name thm = store_thm_open name (export_without_context_open thm);
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
@@ -708,12 +708,12 @@
val protect = Thm.capply (certify Logic.protectC);
val protectI =
- store_thm (Binding.conceal (Binding.name "protectI"))
- (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
+ store_standard_thm (Binding.conceal (Binding.name "protectI"))
+ (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
val protectD =
- store_thm (Binding.conceal (Binding.name "protectD"))
- (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
+ store_standard_thm (Binding.conceal (Binding.name "protectD"))
+ (Thm.equal_elim prop_def (Thm.assume (protect A)));
val protect_cong =
store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
@@ -730,8 +730,8 @@
(* term *)
val termI =
- store_thm (Binding.conceal (Binding.name "termI"))
- (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
+ store_standard_thm (Binding.conceal (Binding.name "termI"))
+ (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
fun mk_term ct =
let
@@ -759,15 +759,14 @@
(* sort_constraint *)
val sort_constraintI =
- store_thm (Binding.conceal (Binding.name "sort_constraintI"))
- (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
+ store_standard_thm (Binding.conceal (Binding.name "sort_constraintI"))
+ (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
val sort_constraint_eq =
- store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
- (standard
- (Thm.equal_intr
- (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
- (implies_intr_list [A, C] (Thm.assume A))));
+ store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+ (Thm.equal_intr
+ (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
+ (implies_intr_list [A, C] (Thm.assume A)));
end;
@@ -983,5 +982,5 @@
end;
-structure BasicDrule: BASIC_DRULE = Drule;
-open BasicDrule;
+structure Basic_Drule: BASIC_DRULE = Drule;
+open Basic_Drule;