# HG changeset patch # User wenzelm # Date 921674824 -3600 # Node ID ed0c7b4a325def33ce251af78b885449f943aa0c # Parent 32fda1090a13b127e23ac5f7bc0718006f5088b0 adapted rep_datatype; diff -r 32fda1090a13 -r ed0c7b4a325d src/HOL/thy_syntax.ML --- a/src/HOL/thy_syntax.ML Wed Mar 17 13:46:23 1999 +0100 +++ b/src/HOL/thy_syntax.ML Wed Mar 17 13:47:04 1999 +0100 @@ -139,8 +139,8 @@ "val thy = thy;\nend;\nval thy = thy\n" end; - fun mk_thmss namess = "(map (PureThy.get_thmss thy) " ^ mk_list (map mk_list namess) ^ ")"; - fun mk_thm name = "(PureThy.get_thm thy " ^ name ^ ")"; + fun mk_thmss namess = mk_list (map (mk_list o map (mk_pair o rpair "[]")) namess); + fun mk_thm name = mk_pair (name, "[]"); fun mk_rep_dt_string (((names, distinct), inject), induct) = ";\nlocal\n\