src/Pure/Isar/theory_target.ML
changeset 25514 4b508bb31a6c
parent 25485 33840a854e63
child 25519 8570745cb40b
     1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:07 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Nov 30 20:13:08 2007 +0100
     1.3 @@ -290,12 +290,7 @@
     1.4      val global_consts = map (Term.dest_Const o Term.head_of o Thm.term_of o Thm.rhs_of o #2) consts;
     1.5  
     1.6      (*axioms*)
     1.7 -    val resubst_instparams = map_aterms (fn t as Free (v, T) =>
     1.8 -      (case Class.instantiation_param lthy' v
     1.9 -       of NONE => t
    1.10 -        | SOME c => Const (c, T)) | t => t)
    1.11 -    val hyps = map Thm.term_of (Assumption.assms_of lthy')
    1.12 -      |> map resubst_instparams;
    1.13 +    val hyps = map Thm.term_of (Assumption.assms_of lthy');
    1.14      fun axiom ((name, atts), props) thy = thy
    1.15        |> fold_map (Thm.add_axiom hyps) (PureThy.name_multi name props)
    1.16        |-> (fn ths => pair ((name, atts), [(ths, [])]));