src/ZF/intr_elim.ML
changeset 202 4e68398cdc06
parent 70 8a29f8b4aca1
child 231 cb6a24451544
--- a/src/ZF/intr_elim.ML	Tue Dec 21 16:27:36 1993 +0100
+++ b/src/ZF/intr_elim.ML	Tue Dec 21 16:38:45 1993 +0100
@@ -204,7 +204,7 @@
 		map (subst_atomic [(Free(X',iT),big_rec_tm)]) parts));
 
 val thy = extend_theory Ind.thy (big_rec_name ^ "_Inductive")
-    ([], [], [], [], [], None) axpairs;
+    ([], [], [], [], [], [], None) axpairs;
 
 val defs = map (get_axiom thy o #1) axpairs;