Avoid nested explicit type annotations

Isabelle does not like nested annotations like "((exp :: typ) :: typ)".

1 files changed, 0 insertions, 17 deletions

diff --git a/src/rewrites.ml b/src/rewrites.ml
index e3f9a93e..9cba6b39 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -103,23 +103,6 @@ let effectful_effs = function
        | _ -> true
       ) effs
 
-
-let lookup_generated_kid env kid =
-  let match_kid_nc kid = function
-    | NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _)
-      when Kid.compare kid kid2 = 0 && not (is_kid_generated kid1) -> kid1
-    | _ -> kid
-  in
-  List.fold_left match_kid_nc kid (Env.get_constraints env)
-
-let add_p_typ typ (P_aux (paux, annot) as pat) =
-  let env = pat_env_of pat in
-  let generated_kids typ = KidSet.filter is_kid_generated (tyvars_of_typ typ) in
-  let subst_kid kid typ = typ_subst_kid kid (lookup_generated_kid env kid) typ in
-  let typ' = KidSet.fold subst_kid (generated_kids typ) typ in
-  if KidSet.is_empty (generated_kids typ') then P_aux (P_typ (typ', pat), annot) else pat
-
-
 let effectful eaux = effectful_effs (effect_of (propagate_exp_effect eaux))
 let effectful_pexp pexp = effectful_effs (snd (propagate_pexp_effect pexp))