# HG changeset patch
# User ballarin
# Date 1117204413 -7200
# Node ID 323838df22fd221f223dc1cad6d01b6895117cc8
# Parent  c5f6726d9bb1652fe4dfe327f9be836fcf58fa7b
Deleted old code.

diff -r c5f6726d9bb1 -r 323838df22fd src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri May 27 16:24:48 2005 +0200
+++ b/src/Pure/Isar/locale.ML	Fri May 27 16:33:33 2005 +0200
@@ -1129,37 +1129,6 @@
 
 local
 
-(* paramify type, process mixfix constraint of renamed syntax *)
-
-fun mx_type _ (x, NONE, mx) = (x, NONE, mx)
-  | mx_type _ (x, SOME T, NONE) =
-      (x, SOME (Term.map_type_tfree (TypeInfer.param 0) T), NONE)
-  | mx_type ctxt (x, SOME T, SOME mx) =
-      let
-val _ = warning "mx_type: mx";
-val _ = PolyML.print mx;
-        val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
-        val T' = Type.varifyT T;
-        val mxTs = map (fn n => TVar ((n, 0), []))
-          (Term.invent_names (Term.add_typ_tfree_names (T, [])) "'a"
-            (Syntax.mixfix_args mx + 1));
-          (* avoid name clashes in unification *)
-        val mxT = mxTs |> Library.split_last |> op --->;
-        val (tenv, _) = Type.unify tsig (Vartab.empty, 0) (T', mxT)
-          handle Type.TUNIFY =>
-            raise TYPE ("failed to satisfy mixfix-constraint for parameter " ^
-              quote x ^ "\nunable to unify", [T', mxT], []);
-        val U = Envir.norm_type tenv T';
-        val ixns = Term.add_typ_ixns ([], U);
-        val ren = Vartab.make (ixns ~~ Term.invent_names [] "'a" (length ixns));
-        val U' = Term.map_type_tvar (fn ((x, i), s) =>
-          (TypeInfer.param 0 (x, s))) U;
-(*        val U' = Term.map_type_tvar (fn (xi, s) =>
-          (TypeInfer.param 0 (valOf (Vartab.lookup (ren, xi)), s))) U;
-*)val _ = warning "mx_type (U, U')";
-val _ = PolyML.print (U, U');
-      in (x, SOME U', SOME mx) end;
-
 fun declare_int_elem (ctxt, Fixes fixes) =
       (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
         (x, Option.map (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])