author | wenzelm |
Sun, 21 Mar 2010 19:30:19 +0100 | |
changeset 35853 | f2126d4d0486 |
parent 35852 | 4e3fe0b8687b |
child 35854 | d452abc96459 |
--- a/src/Pure/more_thm.ML Sun Mar 21 19:28:25 2010 +0100 +++ b/src/Pure/more_thm.ML Sun Mar 21 19:30:19 2010 +0100 @@ -324,7 +324,7 @@ fun add_axiom (b, prop) thy = let - val b' = if Binding.is_empty b then Binding.name ("axiom_" ^ serial_string ()) else b; + val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b; val thy' = thy |> Theory.add_axioms_i [(b', prop)]; val axm = unvarify_global (Thm.axiom thy' (Sign.full_name thy' b')); in (axm, thy') end;