# 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), [])