src/Provers/simplifier.ML
changeset 6556 daa00919502b
parent 6534 5a838c1d9d2f
child 6911 ef0f25d0bc2d
equal deleted inserted replaced
6555:17b7b88a8e3c 6556:daa00919502b
   264 struct
   264 struct
   265   val name = "Provers/simpset";
   265   val name = "Provers/simpset";
   266   type T = simpset ref;
   266   type T = simpset ref;
   267 
   267 
   268   val empty = ref empty_ss;
   268   val empty = ref empty_ss;
   269   fun prep_ext (ref ss) = (ref ss): T;            (*create new reference!*)
   269   fun copy (ref ss) = (ref ss): T;            (*create new reference!*)
       
   270   val prep_ext = copy;
   270   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   271   fun merge (ref ss1, ref ss2) = ref (merge_ss (ss1, ss2));
   271   fun print _ (ref ss) = print_ss ss;
   272   fun print _ (ref ss) = print_ss ss;
   272 end;
   273 end;
   273 
   274 
   274 structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);
   275 structure GlobalSimpset = TheoryDataFun(GlobalSimpsetArgs);