Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 *)
isabelle