declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
authorwenzelm
Wed Sep 26 11:27:46 2007 +0200 (2007-09-26)
changeset 2471921d1cdab2d8c
parent 24718 16b11ba36350
child 24720 4d2f2e375fa1
declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
src/Pure/variable.ML
     1.1 --- a/src/Pure/variable.ML	Wed Sep 26 09:05:58 2007 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Sep 26 11:27:46 2007 +0200
     1.3 @@ -156,10 +156,13 @@
     1.4  
     1.5  (* type occurrences *)
     1.6  
     1.7 +fun decl_type_occsT T = fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I) T;
     1.8 +
     1.9  val decl_type_occs = fold_term_types
    1.10    (fn Free (x, _) => fold_atyps (fn TFree (a, _) => Symtab.insert_list (op =) (a, x) | _ => I)
    1.11 -    | _ => fold_atyps (fn TFree (a, _) => Symtab.default (a, []) | _ => I));
    1.12 +    | _ => decl_type_occsT);
    1.13  
    1.14 +val declare_type_occsT = map_type_occs o fold_types decl_type_occsT;
    1.15  val declare_type_occs = map_type_occs o decl_type_occs;
    1.16  
    1.17  
    1.18 @@ -179,6 +182,7 @@
    1.19          | TVar v => constrain_tvar v
    1.20          | _ => I)) t sorts;
    1.21    in (types', sorts') end)
    1.22 +  #> declare_type_occsT t
    1.23    #> declare_type_names t;
    1.24  
    1.25