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