# HG changeset patch
# User wenzelm
# Date 893843014 -7200
# Node ID fe076613e1228e5b9ff75fbaebe5520367be4bc2
# Parent  cc36acb5b1144e7104fb6ef8277fb646add08c7d
Logic.mk_defpair;
adapted to new PureThy.add_defs_i;

diff -r cc36acb5b114 -r fe076613e122 src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Wed Apr 29 11:42:04 1998 +0200
+++ b/src/HOL/add_ind_def.ML	Wed Apr 29 11:43:34 1998 +0200
@@ -144,7 +144,7 @@
     val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
 
     (*The individual sets must already be declared*)
-    val axpairs = map mk_defpair 
+    val axpairs = map Logic.mk_defpair 
           ((big_rec_tm, lfp_rhs) ::
            (case parts of 
                [_] => []                        (*no mutual recursion*)
@@ -162,7 +162,7 @@
              | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
                                "\n\t*Consider adding type constraints*"))
 
-  in  thy |> PureThy.add_store_defs_i axpairs  end
+  in  thy |> PureThy.add_defs_i (map Attribute.none axpairs)  end
 
 
 end;