simplified export: no Seq.seq;
authorwenzelm
Wed Aug 02 22:26:50 2006 +0200 (2006-08-02)
changeset 20296753fad9f6e03
parent 20295 8b3e97502fd9
child 20297 a9a917b356af
simplified export: no Seq.seq;
normalized Proof.context/method type aliases;
src/Pure/assumption.ML
     1.1 --- a/src/Pure/assumption.ML	Wed Aug 02 22:26:49 2006 +0200
     1.2 +++ b/src/Pure/assumption.ML	Wed Aug 02 22:26:50 2006 +0200
     1.3 @@ -11,13 +11,13 @@
     1.4    val assume_export: export
     1.5    val presume_export: export
     1.6    val assume: cterm -> thm
     1.7 -  val assms_of: Context.proof -> term list
     1.8 -  val prems_of: Context.proof -> thm list
     1.9 -  val extra_hyps: Context.proof -> thm -> term list
    1.10 -  val add_assms: export -> cterm list -> Context.proof -> thm list * Context.proof
    1.11 -  val add_assumes: cterm list -> Context.proof -> thm list * Context.proof
    1.12 -  val add_view: Context.proof -> cterm list -> Context.proof -> Context.proof
    1.13 -  val exports: bool -> Context.proof -> Context.proof -> thm list -> thm list Seq.seq
    1.14 +  val assms_of: Proof.context -> term list
    1.15 +  val prems_of: Proof.context -> thm list
    1.16 +  val extra_hyps: Proof.context -> thm -> term list
    1.17 +  val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
    1.18 +  val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
    1.19 +  val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
    1.20 +  val export: bool -> Proof.context -> Proof.context -> thm -> thm
    1.21  end;
    1.22  
    1.23  structure Assumption: ASSUMPTION =
    1.24 @@ -25,7 +25,7 @@
    1.25  
    1.26  (** basic rules **)
    1.27  
    1.28 -type export = bool -> cterm list -> thm -> thm Seq.seq;
    1.29 +type export = bool -> cterm list -> thm -> thm
    1.30  
    1.31  (*
    1.32      [A]
    1.33 @@ -34,8 +34,8 @@
    1.34    --------
    1.35    #A ==> B
    1.36  *)
    1.37 -fun assume_export true = Seq.single oo Drule.implies_intr_protected
    1.38 -  | assume_export false = Seq.single oo Drule.implies_intr_list;
    1.39 +fun assume_export true = Drule.implies_intr_protected
    1.40 +  | assume_export false = Drule.implies_intr_list;
    1.41  
    1.42  (*
    1.43      [A]
    1.44 @@ -95,16 +95,13 @@
    1.45    in (asms', prems) end);
    1.46  
    1.47  
    1.48 -(* exports *)
    1.49 +(* export *)
    1.50  
    1.51 -fun exports is_goal inner outer =
    1.52 -  let
    1.53 -    val asms = rev (Library.drop (length (assumptions_of outer), assumptions_of inner));
    1.54 -    val exp_asms = map (fn (exp, As) => exp is_goal As) asms;
    1.55 -  in
    1.56 -    map norm_hhf_protect
    1.57 -    #> Seq.map_list (Seq.EVERY exp_asms)
    1.58 -    #> Seq.map (map norm_hhf_protect)
    1.59 +fun export is_goal inner outer =
    1.60 +  let val asms = Library.drop (length (assumptions_of outer), assumptions_of inner) in
    1.61 +    norm_hhf_protect
    1.62 +    #> fold_rev (fn (e, As) => e is_goal As) asms
    1.63 +    #> norm_hhf_protect
    1.64    end;
    1.65  
    1.66  end;