1.1 --- a/src/Pure/more_thm.ML	Wed Sep 03 17:47:40 2008 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Wed Sep 03 17:50:37 2008 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4    val forall_elim_vars: int -> thm -> thm
     1.5    val unvarify: thm -> thm
     1.6    val close_derivation: thm -> thm
     1.7 -  val add_axiom: term list -> bstring * term -> theory -> thm * theory
     1.8 +  val add_axiom: bstring * term -> theory -> thm * theory
     1.9    val add_def: bool -> bool -> bstring * term -> theory -> thm * theory
    1.10    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    1.11    val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
    1.12 @@ -262,15 +262,12 @@
    1.13  
    1.14  (** specification primitives **)
    1.15  
    1.16 -fun add_axiom hyps (name, prop) thy =
    1.17 +fun add_axiom (name, prop) thy =
    1.18    let
    1.19      val name' = if name = "" then "axiom_" ^ serial_string () else name;
    1.20 -    val prop' = Logic.list_implies (hyps, prop);
    1.21 -    val thy' = thy |> Theory.add_axioms_i [(name', prop')];
    1.22 +    val thy' = thy |> Theory.add_axioms_i [(name', prop)];
    1.23      val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name'));
    1.24 -    val prems = map (Thm.assume o Thm.cterm_of thy') hyps;
    1.25 -    val thm = fold elim_implies prems axm;
    1.26 -  in (thm, thy') end;
    1.27 +  in (axm, thy') end;
    1.28  
    1.29  fun add_def unchecked overloaded (name, prop) thy =
    1.30    let