src/Pure/Isar/theory_target.ML
changeset 24987 50b07326da38
parent 24983 f2f4ba67cef1
child 24989 e656aeaa8b28
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 21:10:42 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 21:10:43 2007 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4  structure TheoryTarget: THEORY_TARGET =
     1.5  struct
     1.6  
     1.7 +
     1.8  (** locale targets **)
     1.9  
    1.10  (* context data *)
    1.11 @@ -289,26 +290,18 @@
    1.12  
    1.13  (* defs *)
    1.14  
    1.15 -local
    1.16 -
    1.17 -fun expand_term ctxt t =
    1.18 +fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy =
    1.19    let
    1.20 -    val thy = ProofContext.theory_of ctxt;
    1.21 +    val thy = ProofContext.theory_of lthy;
    1.22      val thy_ctxt = ProofContext.init thy;
    1.23 -    val ct = Thm.cterm_of thy t;
    1.24 -    val (defs, ct') = LocalDefs.export ctxt thy_ctxt (Drule.mk_term ct) ||> Drule.dest_term;
    1.25 -  in (Thm.term_of ct', MetaSimplifier.rewrite true defs ct) end;
    1.26  
    1.27 -in
    1.28 -
    1.29 -fun local_def loc kind ((c, mx), ((name, atts), rhs)) lthy1 =
    1.30 -  let
    1.31 -    val (rhs', rhs_conv) = expand_term lthy1 rhs;
    1.32 -    val xs = Variable.add_fixed (LocalTheory.target_of lthy1) rhs' [];
    1.33 +    val (rhs', rhs_conv) =
    1.34 +      LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
    1.35 +    val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
    1.36      val T = Term.fastype_of rhs;
    1.37  
    1.38      (*consts*)
    1.39 -    val ([(lhs, lhs_def)], lthy2) = lthy1
    1.40 +    val ([(lhs, lhs_def)], lthy2) = lthy
    1.41        |> declare_consts loc (member (op =) xs) [((c, T), mx)];
    1.42      val (_, lhs') = Logic.dest_equals (Thm.prop_of lhs_def);
    1.43  
    1.44 @@ -326,22 +319,26 @@
    1.45        |> local_notes loc kind [((name', atts), [([eq], [])])];
    1.46    in ((lhs, (res_name, res)), lthy4) end;
    1.47  
    1.48 -end;
    1.49 -
    1.50  
    1.51  (* axioms *)
    1.52  
    1.53 -fun axioms loc kind specs lthy =
    1.54 +fun local_axioms loc kind (vars, specs) lthy =
    1.55    let
    1.56      val hyps = map Thm.term_of (Assumption.assms_of lthy);
    1.57      fun axiom ((name, atts), props) thy = thy
    1.58        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    1.59        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.60 +
    1.61 +    val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []);
    1.62 +    val (consts, lthy') = declare_consts loc spec_frees vars lthy;
    1.63 +    val heads = map (Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    1.64    in
    1.65 -    lthy
    1.66 +    lthy'
    1.67 +    |> LocalTheory.theory (Theory.add_finals_i false heads)
    1.68      |> fold (fold Variable.declare_term o snd) specs
    1.69      |> LocalTheory.theory_result (fold_map axiom specs)
    1.70      |-> local_notes loc kind
    1.71 +    |>> pair (map #1 consts)
    1.72    end;
    1.73  
    1.74  
    1.75 @@ -357,8 +354,7 @@
    1.76      |> fold Class.init (the_list (Class.class_of_locale thy loc))
    1.77      |> LocalTheory.init (NameSpace.base loc)
    1.78       {pretty = pretty loc,
    1.79 -      consts = declare_consts loc,
    1.80 -      axioms = axioms loc,
    1.81 +      axioms = local_axioms loc,
    1.82        abbrev = abbrev loc,
    1.83        def = local_def loc,
    1.84        notes = local_notes loc,