--- a/src/Pure/Syntax/sextension.ML Mon Oct 11 12:30:06 1993 +0100
+++ b/src/Pure/Syntax/sextension.ML Mon Oct 11 12:30:38 1993 +0100
@@ -42,7 +42,6 @@
val eta_contract: bool ref
val mk_binder_tr: string * string -> string * (term list -> term)
val mk_binder_tr': string * string -> string * (term list -> term)
- val ndependent_tr: string -> term list -> term (* FIXME remove *)
val dependent_tr': string * string -> term list -> term
val max_pri: int
end
@@ -215,13 +214,6 @@
| bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
-(* 'dependent' type operators *) (* FIXME remove *)
-
-fun ndependent_tr q [A, B] =
- Const (q, dummyT) $ A $ Abs ("x", dummyT, incr_boundvars 1 B)
- | ndependent_tr _ ts = raise_term "ndependent_tr" ts;
-
-
(** print (ast) translations **)