normalized Proof.context/method type aliases;
simplified Assumption/ProofContext.export;

--- a/src/Pure/Isar/local_defs.ML	Wed Aug 02 22:26:59 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Wed Aug 02 22:27:00 2006 +0200
@@ -7,23 +7,22 @@
 
 signature LOCAL_DEFS =
 sig
-  val cert_def: ProofContext.context -> term -> (string * typ) * term
+  val cert_def: Proof.context -> term -> (string * typ) * term
   val abs_def: term -> (string * typ) * term
-  val mk_def: ProofContext.context -> (string * term) list -> term list
+  val mk_def: Proof.context -> (string * term) list -> term list
   val def_export: Assumption.export
-  val add_def: string * term -> ProofContext.context ->
-    ((string * typ) * thm) * ProofContext.context
+  val add_def: string * term -> Proof.context -> ((string * typ) * thm) * Proof.context
   val print_rules: Context.generic -> unit
   val defn_add: attribute
   val defn_del: attribute
   val meta_rewrite_rule: Context.generic -> thm -> thm
-  val unfold: ProofContext.context -> thm list -> thm -> thm
-  val unfold_goals: ProofContext.context -> thm list -> thm -> thm
-  val unfold_tac: ProofContext.context -> thm list -> tactic
-  val fold: ProofContext.context -> thm list -> thm -> thm
-  val fold_tac: ProofContext.context -> thm list -> tactic
-  val derived_def: ProofContext.context -> bool -> term ->
-    ((string * typ) * term) * (ProofContext.context -> term -> thm -> thm)
+  val unfold: Proof.context -> thm list -> thm -> thm
+  val unfold_goals: Proof.context -> thm list -> thm -> thm
+  val unfold_tac: Proof.context -> thm list -> tactic
+  val fold: Proof.context -> thm list -> thm -> thm
+  val fold_tac: Proof.context -> thm list -> tactic
+  val derived_def: Proof.context -> bool -> term ->
+    ((string * typ) * term) * (Proof.context -> term -> thm -> thm)
 end;
 
 structure LocalDefs: LOCAL_DEFS =
@@ -67,11 +66,11 @@
   -----------
       B t
 *)
-fun def_export _ cprops thm =
+fun def_export _ defs thm =
   thm
-  |> Drule.implies_intr_list cprops
-  |> Drule.generalize ([], map head_of_def cprops)
-  |> RANGE (replicate (length cprops) (Tactic.rtac Drule.reflexive_thm)) 1;
+  |> Drule.implies_intr_list defs
+  |> Drule.generalize ([], map head_of_def defs)
+  |> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
 
 
 (* add defs *)