adapted add_trfunsT;
authorwenzelm
Wed Nov 05 11:34:44 1997 +0100 (1997-11-05)
changeset 4141b76a49490833
parent 4140 c62df16811fe
child 4142 d182dc0a34f6
adapted add_trfunsT;
defs: admit TYPE arguments;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Wed Nov 05 11:33:45 1997 +0100
     1.2 +++ b/src/Pure/theory.ML	Wed Nov 05 11:34:44 1997 +0100
     1.3 @@ -60,7 +60,7 @@
     1.4      (bstring * (term list -> term)) list *
     1.5      (bstring * (Syntax.ast list -> Syntax.ast)) list -> theory -> theory
     1.6    val add_trfunsT:
     1.7 -    (bstring * (typ -> term list -> term)) list -> theory -> theory
     1.8 +    (bstring * (bool -> typ -> term list -> term)) list -> theory -> theory
     1.9    val add_tokentrfuns:
    1.10      (string * string * (string -> string * int)) list -> theory -> theory
    1.11    val add_trrules: (string * string) Syntax.trrule list -> theory -> theory
    1.12 @@ -310,14 +310,18 @@
    1.13        | occs_const (t $ u) = occs_const t orelse occs_const u
    1.14        | occs_const _ = false;
    1.15  
    1.16 -    val show_frees = commas_quote o map (fst o dest_Free);
    1.17 +    fun dest_free (Free (x, _)) = x
    1.18 +      | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
    1.19 +      | dest_free _ = raise Match;
    1.20 +
    1.21 +    val show_frees = commas_quote o map dest_free;
    1.22      val show_tfrees = commas_quote o map fst;
    1.23  
    1.24      val lhs_dups = duplicates args;
    1.25      val rhs_extras = gen_rems (op =) (term_frees rhs, args);
    1.26      val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
    1.27    in
    1.28 -    if not (forall is_Free args) then
    1.29 +    if not (forall (can dest_free) args) then
    1.30        err "Arguments (on lhs) must be variables"
    1.31      else if not (null lhs_dups) then
    1.32        err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)