src/ZF/Tools/typechk.ML
changeset 6556 daa00919502b
parent 6153 bff90585cce5
child 12109 bd6eb9194a5d
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
    92 structure TypecheckingArgs =
    92 structure TypecheckingArgs =
    93   struct
    93   struct
    94   val name = "ZF/type-checker";
    94   val name = "ZF/type-checker";
    95   type T = tcset ref;
    95   type T = tcset ref;
    96   val empty = ref (TC{rules=[], net=Net.empty});
    96   val empty = ref (TC{rules=[], net=Net.empty});
    97   fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
    97   fun copy (ref tc) = ref tc;
       
    98   val prep_ext = copy;
    98   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    99   fun merge (ref tc1, ref tc2) = ref (merge_tc (tc1, tc2));
    99   fun print _ (ref tc) = print_tc tc;
   100   fun print _ (ref tc) = print_tc tc;
   100   end;
   101   end;
   101 
   102 
   102 structure TypecheckingData = TheoryDataFun(TypecheckingArgs);
   103 structure TypecheckingData = TheoryDataFun(TypecheckingArgs);