# HG changeset patch
# User clasohm
# Date 826117901 -3600
# Node ID a5f48457dfd530cb8c4be095d51dece32feaf169
# Parent  4ee99a973be4fa512dd1048bdfab0c48d04f4642
added constdefs

diff -r 4ee99a973be4 -r a5f48457dfd5 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Wed Mar 06 14:10:44 1996 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Wed Mar 06 14:11:41 1996 +0100
@@ -351,6 +351,22 @@
 val axiom_decls = repeat1 (ident -- !! string) >> mk_axiom_decls;
 
 
+(* combined consts and axioms *)
+
+fun mk_constaxiom_decls x =
+  let
+    val (axms_defs, axms_names) =
+      mk_axiom_decls (map (fn ((id, _), def) => (id ^ "_def", def)) x);
+  in ((mk_big_list o map mk_triple2 o map (apfst quote o fst)) x ^
+       "\n\n|> add_defs\n" ^ axms_defs, axms_names)
+  end;
+
+val constaxiom_decls =
+  repeat1 (ident --$$ "::" -- !!
+           ((string || const_type false >> quote) -- opt_mixfix) -- !!
+           string) >> mk_constaxiom_decls;
+
+
 (* axclass *)
 
 fun mk_axclass_decl ((c, cs), axms) =
@@ -516,6 +532,7 @@
   section "MLtext" "" verbatim,
   axm_section "rules" "|> add_axioms" axiom_decls,
   axm_section "defs" "|> add_defs" axiom_decls,
+  axm_section "constdefs" "|> add_consts" constaxiom_decls,
   axm_section "axclass" "|> AxClass.add_axclass" axclass_decl,
   section "instance" "" instance_decl];