src/Pure/Isar/proof_context.ML
changeset 11816 545aab7410ac
parent 11793 5f0ab6f5c280
child 11915 df030220a2a8
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:00:21 2001 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 16 23:02:14 2001 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    val generalizeT: context -> context -> typ -> typ
     1.5    val generalize: context -> context -> term -> term
     1.6    val find_free: term -> string -> term option
     1.7 -  val export_wrt: bool -> context -> context option -> (thm -> thm Seq.seq) * (int -> tactic) list
     1.8 +  val export_wrt: bool -> context -> context option -> thm -> thm Seq.seq
     1.9    val drop_schematic: indexname * term option -> indexname * term option
    1.10    val add_binds: (indexname * string option) list -> context -> context
    1.11    val add_binds_i: (indexname * term option) list -> context -> context
    1.12 @@ -120,8 +120,7 @@
    1.13  
    1.14  (** datatype context **)
    1.15  
    1.16 -type exporter =
    1.17 -  (cterm list -> thm -> thm Seq.seq) * (bool -> int -> (int -> tactic) list);
    1.18 +type exporter = bool -> cterm list -> thm -> thm Seq.seq;
    1.19  
    1.20  datatype context =
    1.21    Context of
    1.22 @@ -578,40 +577,31 @@
    1.23  
    1.24  fun find_free t x = foldl_aterms (get_free x) (None, t);
    1.25  
    1.26 -
    1.27 -local
    1.28 -
    1.29 -fun export tfrees fixes goal_asms thm =
    1.30 -  thm
    1.31 -  |> Tactic.norm_hhf
    1.32 -  |> Seq.EVERY (rev (map op |> goal_asms))
    1.33 -  |> Seq.map (fn rule =>
    1.34 -    let
    1.35 -      val {sign, prop, maxidx, ...} = Thm.rep_thm rule;
    1.36 -      val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
    1.37 -    in
    1.38 -      rule
    1.39 -      |> Drule.forall_intr_list frees
    1.40 -      |> Tactic.norm_hhf
    1.41 -      |> Drule.tvars_intr_list tfrees
    1.42 -    end);
    1.43 -
    1.44  fun diff_context inner None = (gen_tfrees inner None, fixed_names inner, assumptions inner)
    1.45    | diff_context inner (Some outer) =
    1.46        (gen_tfrees inner (Some outer),
    1.47          fixed_names inner \\ fixed_names outer,
    1.48          Library.drop (length (assumptions outer), assumptions inner));
    1.49  
    1.50 -in
    1.51 -
    1.52  fun export_wrt is_goal inner opt_outer =
    1.53    let
    1.54      val (tfrees, fixes, asms) = diff_context inner opt_outer;
    1.55 -    val goal_asms = map (fn (cprops, (exp, _)) => (map Drule.mk_cgoal cprops, exp)) asms;
    1.56 -    val tacs = flat (map (fn (cprops, (_, f)) => f is_goal (length cprops)) asms);
    1.57 -  in (export tfrees fixes goal_asms, tacs) end;
    1.58 -
    1.59 -end;
    1.60 +    val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
    1.61 +  in fn thm =>
    1.62 +    thm
    1.63 +    |> Tactic.norm_hhf
    1.64 +    |> Seq.EVERY (rev exp_asms)
    1.65 +    |> Seq.map (fn rule =>
    1.66 +      let
    1.67 +        val {sign, prop, ...} = Thm.rep_thm rule;
    1.68 +        val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes);
    1.69 +      in
    1.70 +        rule
    1.71 +        |> Drule.forall_intr_list frees
    1.72 +        |> Tactic.norm_hhf
    1.73 +        |> Drule.tvars_intr_list tfrees
    1.74 +      end)
    1.75 +  end;
    1.76  
    1.77  
    1.78  
    1.79 @@ -849,7 +839,7 @@
    1.80  fun add_assm (ctxt, ((name, attrs), props)) =
    1.81    let
    1.82      val cprops = map (Thm.cterm_of (sign_of ctxt)) props;
    1.83 -    val asms = map (Tactic.norm_hhf o Drule.assume_goal) cprops;
    1.84 +    val asms = map (Tactic.norm_hhf o Thm.assume) cprops;
    1.85  
    1.86      val ths = map (fn th => ([th], [])) asms;
    1.87      val (ctxt', [(_, thms)]) =