src/ZF/Tools/typechk.ML
changeset 6556 daa00919502b
parent 6153 bff90585cce5
child 12109 bd6eb9194a5d
     1.1 --- a/src/ZF/Tools/typechk.ML	Fri Apr 30 18:09:33 1999 +0200
     1.2 +++ b/src/ZF/Tools/typechk.ML	Fri Apr 30 18:10:03 1999 +0200
     1.3 @@ -94,7 +94,8 @@
     1.4    val name = "ZF/type-checker";
     1.5    type T = tcset ref;
     1.6    val empty = ref (TC{rules=[], net=Net.empty});
     1.7 -  fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
     1.8 +  fun copy (ref tc) = ref tc;
     1.9 +  val prep_ext = copy;
    1.10    fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    1.11    fun print _ (ref tc) = print_tc tc;
    1.12    end;