# HG changeset patch # User wenzelm # Date 878726084 -3600 # Node ID b76a494908332640b3b233ad1b633821f11f6b1e # Parent c62df16811fe0644078615bc217b5bfaa31f65b0 adapted add_trfunsT; defs: admit TYPE arguments; diff -r c62df16811fe -r b76a49490833 src/Pure/theory.ML --- a/src/Pure/theory.ML Wed Nov 05 11:33:45 1997 +0100 +++ b/src/Pure/theory.ML Wed Nov 05 11:34:44 1997 +0100 @@ -60,7 +60,7 @@ (bstring * (term list -> term)) list * (bstring * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory val add_trfunsT: - (bstring * (typ -> term list -> term)) list -> theory -> theory + (bstring * (bool -> typ -> term list -> term)) list -> theory -> theory val add_tokentrfuns: (string * string * (string -> string * int)) list -> theory -> theory val add_trrules: (string * string) Syntax.trrule list -> theory -> theory @@ -310,14 +310,18 @@ | occs_const (t $ u) = occs_const t orelse occs_const u | occs_const _ = false; - val show_frees = commas_quote o map (fst o dest_Free); + fun dest_free (Free (x, _)) = x + | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x + | dest_free _ = raise Match; + + val show_frees = commas_quote o map dest_free; val show_tfrees = commas_quote o map fst; val lhs_dups = duplicates args; val rhs_extras = gen_rems (op =) (term_frees rhs, args); val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty); in - if not (forall is_Free args) then + if not (forall (can dest_free) args) then err "Arguments (on lhs) must be variables" else if not (null lhs_dups) then err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)