# HG changeset patch
# User wenzelm
# Date 750339038 -3600
# Node ID bc48a71464b02aa6ded0aca8aa4f70729747489b
# Parent  0af9dbb93529853b146cd6e3349204ca39ddf46c
removed ndependent_tr (no longer needed, use _K);

diff -r 0af9dbb93529 -r bc48a71464b0 src/Pure/Syntax/sextension.ML
--- 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 **)