# HG changeset patch
# User wenzelm
# Date 777305543 -7200
# Node ID 01c043f610772bd09bd7a38effa152cbb995bbec
# Parent  959cb0e329f7850fe98ba66490bdfb58e1851b5f
replaced add_defns_i by add_defs_i;

diff -r 959cb0e329f7 -r 01c043f61077 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Fri Aug 19 16:09:27 1994 +0200
+++ b/src/ZF/add_ind_def.ML	Fri Aug 19 16:12:23 1994 +0200
@@ -169,7 +169,7 @@
 	     | _ => rec_tms ~~		(*define the sets as Parts*)
 		    map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
-  in  thy |> add_defns_i axpairs  end
+  in  thy |> add_defs_i axpairs  end
 
 
 (*external, string-based version; needed?*)
@@ -259,9 +259,5 @@
     val axpairs =
 	big_case_def :: flat (map mk_con_defs ((1 upto npart) ~~ con_ty_lists))
 
-    in  thy |> add_consts_i const_decs |> add_defns_i axpairs  end;
+    in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
 end;
-
-
-
-