src/FOLP/hypsubst.ML

     (*exported purely for debugging purposes*)
   val eq_var              : bool -> term -> int * thm
   val inspect_pair        : bool -> term * term -> thm
   end;
 
-functor HypsubstFun(Data: HYPSUBST_DATA): HYPSUBST =
+functor Hypsubst(Data: HYPSUBST_DATA): HYPSUBST =
 struct
 
 local open Data in
 
 exception EQ_VAR;