# HG changeset patch # User wenzelm # Date 1220457037 -7200 # Node ID cd2547ab0696cf3d6b6405cf9b9e454a37027e83 # Parent cd0d170d4dc6084d0e6f0a40b3911c8aae52cb4b simplified add_axiom: no hyps; diff -r cd0d170d4dc6 -r cd2547ab0696 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Wed Sep 03 17:47:40 2008 +0200 +++ b/src/Pure/more_thm.ML Wed Sep 03 17:50:37 2008 +0200 @@ -38,7 +38,7 @@ val forall_elim_vars: int -> thm -> thm val unvarify: thm -> thm val close_derivation: thm -> thm - val add_axiom: term list -> bstring * term -> theory -> thm * theory + val add_axiom: bstring * term -> theory -> thm * theory val add_def: bool -> bool -> bstring * term -> theory -> thm * theory val rule_attribute: (Context.generic -> thm -> thm) -> attribute val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute @@ -262,15 +262,12 @@ (** specification primitives **) -fun add_axiom hyps (name, prop) thy = +fun add_axiom (name, prop) thy = let val name' = if name = "" then "axiom_" ^ serial_string () else name; - val prop' = Logic.list_implies (hyps, prop); - val thy' = thy |> Theory.add_axioms_i [(name', prop')]; + val thy' = thy |> Theory.add_axioms_i [(name', prop)]; val axm = unvarify (Thm.get_axiom_i thy' (Sign.full_name thy' name')); - val prems = map (Thm.assume o Thm.cterm_of thy') hyps; - val thm = fold elim_implies prems axm; - in (thm, thy') end; + in (axm, thy') end; fun add_def unchecked overloaded (name, prop) thy = let