# HG changeset patch
# User wenzelm
# Date 878057775 -3600
# Node ID b94dc94be4b7e307a791d57098ad094cfa15f06a
# Parent  77e426be562413ef5bbc079464e16de49469d5d7
PureThy.add_store_axioms;

diff -r 77e426be5624 -r b94dc94be4b7 src/Cube/Cube.ML
--- a/src/Cube/Cube.ML	Tue Oct 28 17:41:40 1997 +0100
+++ b/src/Cube/Cube.ML	Tue Oct 28 17:56:15 1997 +0100
@@ -12,7 +12,7 @@
 
 val L2_thy =
   Cube.thy
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
     ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
@@ -25,7 +25,7 @@
 
 val Lomega_thy =
   Cube.thy
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
     ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
@@ -40,7 +40,7 @@
 
 val LP_thy =
   Cube.thy
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
     ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
diff -r 77e426be5624 -r b94dc94be4b7 src/LCF/ex/ex.ML
--- a/src/LCF/ex/ex.ML	Tue Oct 28 17:41:40 1997 +0100
+++ b/src/LCF/ex/ex.ML	Tue Oct 28 17:56:15 1997 +0100
@@ -16,7 +16,7 @@
     ("G", "'a => 'a", NoSyn),
     ("H", "'a => 'a", NoSyn),
     ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("P_strict", "P(UU) = UU"),
     ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
     ("H", "H = FIX(K)")]
@@ -61,7 +61,7 @@
     ("G", "'a => 'a", NoSyn),
     ("H", "'a => 'b => 'b", NoSyn),
     ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("F_strict", "F(UU) = UU"),
     ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
     ("H", "H = FIX(K)")]
@@ -90,7 +90,7 @@
   |> Theory.add_consts
    [("s", "'a => 'a", NoSyn),
     ("p", "'a => 'a => 'a", NoSyn)]
-  |> Theory.add_axioms
+  |> PureThy.add_store_axioms
    [("p_strict", "p(UU) = UU"),
     ("p_s", "p(s(x),y) = s(p(x,y))")]
   |> Theory.add_name "fix ex";