inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
authorwenzelm
Mon Mar 22 19:26:12 2010 +0100 (2010-03-22 ago)
changeset 35896487b267433b1
parent 35895 387de5db0a74
child 35897 8758895ea413
inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Mon Mar 22 19:25:14 2010 +0100
     1.2 +++ b/src/Pure/axclass.ML	Mon Mar 22 19:26:12 2010 +0100
     1.3 @@ -514,6 +514,12 @@
     1.4  
     1.5  local
     1.6  
     1.7 +(* old-style axioms *)
     1.8 +
     1.9 +fun add_axiom (b, prop) =
    1.10 +  Thm.add_axiom (b, prop) #->
    1.11 +  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    1.12 +
    1.13  fun axiomatize prep mk name add raw_args thy =
    1.14    let
    1.15      val args = prep thy raw_args;
    1.16 @@ -521,7 +527,7 @@
    1.17      val names = name args;
    1.18    in
    1.19      thy
    1.20 -    |> fold_map Drule.add_axiom (map Binding.name names ~~ specs)
    1.21 +    |> fold_map add_axiom (map Binding.name names ~~ specs)
    1.22      |-> fold add
    1.23    end;
    1.24