src/ZF/ind_syntax.ML
changeset 202 4e68398cdc06
parent 70 8a29f8b4aca1
child 231 cb6a24451544
--- a/src/ZF/ind_syntax.ML	Tue Dec 21 16:27:36 1993 +0100
+++ b/src/ZF/ind_syntax.ML	Tue Dec 21 16:38:45 1993 +0100
@@ -19,7 +19,7 @@
 fun thy addconsts const_decs = 
     extend_theory thy (space_implode "_" (flat (map #1 const_decs)) 
 		       ^ "_Theory")
-		  ([], [], [], [], const_decs, None) [];
+		  ([], [], [], [], [], const_decs, None) [];
 
 
 (*Make a definition, lhs==rhs, checking that vars on lhs contain *)