thmref: Name vs. NameSelection;
authorwenzelm
Mon Jun 20 22:14:15 2005 +0200 (2005-06-20)
changeset 16501fec0cf020bad
parent 16500 09d43301b195
child 16502 5a56e59526a5
thmref: Name vs. NameSelection;
tuned;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Jun 20 22:14:14 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Jun 20 22:14:15 2005 +0200
     1.3 @@ -496,13 +496,13 @@
     1.4  (** prepare terms and propositions **)
     1.5  
     1.6  (*
     1.7 -  (1) read / certify wrt. signature of context
     1.8 +  (1) read / certify wrt. theory of context
     1.9    (2) intern Skolem constants
    1.10    (3) expand term bindings
    1.11  *)
    1.12  
    1.13  
    1.14 -(* read / certify wrt. signature *)     (*exception ERROR*) (*exception TERM*)
    1.15 +(* read wrt. theory *)     (*exception ERROR*)
    1.16  
    1.17  fun read_def_termTs freeze pp syn thy (types, sorts, used) sTs =
    1.18    Sign.read_def_terms' pp (Sign.is_logtype thy) syn (thy, types, sorts) used freeze sTs;
    1.19 @@ -523,13 +523,6 @@
    1.20    #1 o read_def_termTs freeze pp syn thy defs o map (rpair propT);
    1.21  
    1.22  
    1.23 -fun cert_term_thy pp thy t = #1 (Sign.certify_term pp thy t);
    1.24 -
    1.25 -fun cert_prop_thy pp thy tm =
    1.26 -  let val (t, T, _) = Sign.certify_term pp thy tm
    1.27 -  in if T = propT then t else raise TERM ("Term not of type prop", [t]) end;
    1.28 -
    1.29 -
    1.30  (* norm_term *)
    1.31  
    1.32  (*beta normal form for terms (not eta normal form), chase variables in
    1.33 @@ -626,16 +619,20 @@
    1.34  fun gen_cert cert pattern schematic ctxt t = t
    1.35    |> (if pattern then I else norm_term ctxt schematic)
    1.36    |> (fn t' => cert (pp ctxt) (theory_of ctxt) t'
    1.37 -    handle TERM (msg, _) => raise CONTEXT (msg, ctxt));
    1.38 +    handle TYPE (msg, _, _) => raise CONTEXT (msg, ctxt)
    1.39 +      | TERM (msg, _) => raise CONTEXT (msg, ctxt));
    1.40 +
    1.41 +val certify_term = #1 ooo Sign.certify_term;
    1.42 +val certify_prop = #1 ooo Sign.certify_prop;
    1.43  
    1.44  in
    1.45  
    1.46 -val cert_term = gen_cert cert_term_thy false false;
    1.47 -val cert_prop = gen_cert cert_prop_thy false false;
    1.48 -val cert_props = map oo gen_cert cert_prop_thy false;
    1.49 +val cert_term = gen_cert certify_term false false;
    1.50 +val cert_prop = gen_cert certify_prop false false;
    1.51 +val cert_props = map oo gen_cert certify_prop false;
    1.52  
    1.53 -fun cert_term_pats _ = map o gen_cert cert_term_thy true false;
    1.54 -val cert_prop_pats = map o gen_cert cert_prop_thy true false;
    1.55 +fun cert_term_pats _ = map o gen_cert certify_term true false;
    1.56 +val cert_prop_pats = map o gen_cert certify_prop true false;
    1.57  
    1.58  end;
    1.59  
    1.60 @@ -974,15 +971,18 @@
    1.61  (* get_thm(s) *)
    1.62  
    1.63  (*beware of proper order of evaluation!*)
    1.64 -fun retrieve_thms f g (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
    1.65 -  let
    1.66 -    val thy_ref = Theory.self_ref thy;
    1.67 -    val get_from_thy = f thy;
    1.68 -  in
    1.69 -    fn xnamei as (xname, _) =>
    1.70 -      (case Symtab.lookup (tab, NameSpace.intern space xname) of
    1.71 -        SOME ths => map (Thm.transfer (Theory.deref thy_ref)) (PureThy.select_thm xnamei ths)
    1.72 -      | _ => get_from_thy xnamei) |> g xname
    1.73 +fun retrieve_thms from_thy pick (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
    1.74 +  let val thy_ref = Theory.self_ref thy in
    1.75 +    fn xthmref =>
    1.76 +      let
    1.77 +        val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
    1.78 +        val name = PureThy.name_of_thmref thmref;
    1.79 +        val thy' = Theory.deref thy_ref;
    1.80 +      in
    1.81 +        (case Symtab.lookup (tab, name) of
    1.82 +          SOME ths => map (Thm.transfer thy') (PureThy.select_thm thmref ths)
    1.83 +        | NONE => from_thy thy' xthmref) |> pick name
    1.84 +      end
    1.85    end;
    1.86  
    1.87  val get_thm = retrieve_thms PureThy.get_thms PureThy.single_thm;
    1.88 @@ -994,7 +994,7 @@
    1.89  (* valid_thms *)
    1.90  
    1.91  fun valid_thms ctxt (name, ths) =
    1.92 -  (case try (transform_error (fn () => get_thms ctxt (name, NONE))) () of
    1.93 +  (case try (transform_error (fn () => get_thms ctxt (Name name))) () of
    1.94      NONE => false
    1.95    | SOME ths' => Thm.eq_thms (ths, ths'));
    1.96