1.1 --- a/src/Pure/Syntax/sextension.ML	Mon Oct 11 12:30:06 1993 +0100
     1.2 +++ b/src/Pure/Syntax/sextension.ML	Mon Oct 11 12:30:38 1993 +0100
     1.3 @@ -42,7 +42,6 @@
     1.4      val eta_contract: bool ref
     1.5      val mk_binder_tr: string * string -> string * (term list -> term)
     1.6      val mk_binder_tr': string * string -> string * (term list -> term)
     1.7 -    val ndependent_tr: string -> term list -> term    (* FIXME remove *)
     1.8      val dependent_tr': string * string -> term list -> term
     1.9      val max_pri: int
    1.10    end
    1.11 @@ -215,13 +214,6 @@
    1.12    | bigimpl_ast_tr (*"_bigimpl"*) asts = raise_ast "bigimpl_ast_tr" asts;
    1.13  
    1.14  
    1.15 -(* 'dependent' type operators *)  (* FIXME remove *)
    1.16 -
    1.17 -fun ndependent_tr q [A, B] =
    1.18 -      Const (q, dummyT) $ A $ Abs ("x", dummyT, incr_boundvars 1 B)
    1.19 -  | ndependent_tr _ ts = raise_term "ndependent_tr" ts;
    1.20 -
    1.21 -
    1.22  
    1.23  (** print (ast) translations **)
    1.24