--- a/src/Pure/Syntax/syntax.ML Thu Nov 25 11:37:51 1993 +0100
+++ b/src/Pure/Syntax/syntax.ML Thu Nov 25 11:39:45 1993 +0100
@@ -8,7 +8,6 @@
extend_tables (requires extend_gram) (roots!)
replace add_synrules by extend_tables
extend, merge: make roots handling more robust
- extend: read_typ (incl check) as arg, remove def_sort
extend: use extend_tables
*)
@@ -22,14 +21,14 @@
include PRINTER0
type syntax
val type_syn: syntax
- val extend: syntax * (indexname -> sort) -> string list * string list * sext
- -> syntax
+ val extend: syntax -> (string -> typ) -> string list * string list * sext -> syntax
val merge: syntax * syntax -> syntax
val print_gram: syntax -> unit
val print_trans: syntax -> unit
val print_syntax: syntax -> unit
val test_read: syntax -> string -> string -> unit
val read: syntax -> typ -> string -> term
+ val read_typ: syntax -> (indexname -> sort) -> string -> typ
val pretty_term: syntax -> term -> Pretty.T
val pretty_typ: syntax -> typ -> Pretty.T
val string_of_term: syntax -> term -> string
@@ -316,6 +315,12 @@
+(** read_typ **)
+
+fun read_typ syn def_sort str = typ_of_term def_sort (read syn typeT str);
+
+
+
(** read_rule **)
fun read_rule syn (xrule as ((_, lhs_src), (_, rhs_src))) =
@@ -390,10 +395,9 @@
(** extend **)
-fun extend (old_syn as Syntax (ggr, _), def_sort) (roots, xconsts, sext) =
+fun extend (old_syn as Syntax (ggr, _)) read_ty (roots, xconsts, sext) =
let
- fun read_typ s = typ_of_term def_sort (read old_syn typeT s);
- val ext = ext_of_sext roots xconsts read_typ sext;
+ val ext = ext_of_sext roots xconsts read_ty sext;
val (tmp_syn as Syntax (_, tmp_tabs)) =
make_syntax (ref (ExtGG (ggr, (ext, empty_synrules))));