export: added explicit term operation;
authorwenzelm
Wed Dec 06 21:19:03 2006 +0100 (2006-12-06)
changeset 216864f5f6c685ab4
parent 21685 8f3c07f4152d
child 21687 f689f729afab
export: added explicit term operation;
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 06 21:19:02 2006 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 06 21:19:03 2006 +0100
     1.3 @@ -873,9 +873,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun axioms_export axs _ hyps =
     1.8 -  Element.satisfy_thm axs
     1.9 -  #> Drule.implies_intr_list (Library.drop (length axs, hyps));
    1.10 +fun axioms_export axs _ As =
    1.11 +  (Element.satisfy_thm axs #> Drule.implies_intr_list (Library.drop (length axs, As)), fn t => t);
    1.12  
    1.13  
    1.14  (* NB: derived ids contain only facts at this stage *)
     2.1 --- a/src/Pure/Isar/obtain.ML	Wed Dec 06 21:19:02 2006 +0100
     2.2 +++ b/src/Pure/Isar/obtain.ML	Wed Dec 06 21:19:03 2006 +0100
     2.3 @@ -64,16 +64,21 @@
     2.4    --------
     2.5       B
     2.6  *)
     2.7 -fun obtain_export fix_ctxt rule xs _ As thm =
     2.8 +fun eliminate_term ctxt xs tm =
     2.9 +  let
    2.10 +    val vs = map (dest_Free o Thm.term_of) xs;
    2.11 +    val bads = Term.fold_aterms (fn t as Free v =>
    2.12 +      if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
    2.13 +    val _ = null bads orelse
    2.14 +      error ("Result contains obtained parameters: " ^
    2.15 +        space_implode " " (map (ProofContext.string_of_term ctxt) bads));
    2.16 +  in tm end;
    2.17 +
    2.18 +fun eliminate fix_ctxt rule xs As thm =
    2.19    let
    2.20      val thy = ProofContext.theory_of fix_ctxt;
    2.21  
    2.22 -    val vs = map (dest_Free o Thm.term_of) xs;
    2.23 -    val bads = Term.fold_aterms (fn t as Free v =>
    2.24 -      if member (op =) vs v then insert (op aconv) t else I | _ => I) (Thm.prop_of thm) [];
    2.25 -    val _ = null bads orelse
    2.26 -      error ("Result contains obtained parameters: " ^
    2.27 -        space_implode " " (map (ProofContext.string_of_term fix_ctxt) bads));
    2.28 +    val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
    2.29      val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
    2.30        error "Conclusion in obtained context must be object-logic judgment";
    2.31  
    2.32 @@ -88,6 +93,9 @@
    2.33      |> singleton (Variable.export ctxt' fix_ctxt)
    2.34    end;
    2.35  
    2.36 +fun obtain_export ctxt rule xs _ As =
    2.37 +  (eliminate ctxt rule xs As, eliminate_term ctxt xs);
    2.38 +
    2.39  
    2.40  
    2.41  (** obtain **)