src/Pure/Isar/theory_target.ML
changeset 24989 e656aeaa8b28
parent 24987 50b07326da38
child 25002 c3d9cb390471
     1.1 --- a/src/Pure/Isar/theory_target.ML	Thu Oct 11 21:44:28 2007 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Oct 11 23:03:11 2007 +0200
     1.3 @@ -324,14 +324,14 @@
     1.4  
     1.5  fun local_axioms loc kind (vars, specs) lthy =
     1.6    let
     1.7 -    val hyps = map Thm.term_of (Assumption.assms_of lthy);
     1.8 +    val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []);
     1.9 +    val (consts, lthy') = declare_consts loc spec_frees vars lthy;
    1.10 +    val heads = map (Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    1.11 +
    1.12 +    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    1.13      fun axiom ((name, atts), props) thy = thy
    1.14        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    1.15        |-> (fn ths => pair ((name, atts), [(ths, [])]));
    1.16 -
    1.17 -    val spec_frees = member (op =) (fold (fold Term.add_frees o snd) specs []);
    1.18 -    val (consts, lthy') = declare_consts loc spec_frees vars lthy;
    1.19 -    val heads = map (Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
    1.20    in
    1.21      lthy'
    1.22      |> LocalTheory.theory (Theory.add_finals_i false heads)