# HG changeset patch
# User wenzelm
# Date 1085167187 -7200
# Node ID 5bb4bbdb6529a01213aed4799adb1bee0470bdbb
# Parent  4f3b383a46aee7af103ee777334c5ef8907cddf7
TypeInfer.paramify_dummies, TypeInfer.param;

diff -r 4f3b383a46ae -r 5bb4bbdb6529 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri May 21 21:19:18 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Fri May 21 21:19:47 2004 +0200
@@ -482,7 +482,7 @@
 fun unify_frozen ctxt maxidx Ts Us =
   let
     fun paramify (i, None) = (i, None)
-      | paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T));
+      | paramify (i, Some T) = apsnd Some (TypeInfer.paramify_dummies (i, T));
 
     val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
     val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
@@ -757,7 +757,7 @@
 
 fun declare_int_elem (ctxt, Fixes fixes) =
       (ctxt |> ProofContext.add_fixes (map (fn (x, T, mx) =>
-        (x, apsome (Term.map_type_tfree (Type.param 0)) T, mx)) fixes), [])
+        (x, apsome (Term.map_type_tfree (TypeInfer.param 0)) T, mx)) fixes), [])
   | declare_int_elem (ctxt, _) = (ctxt, []);
 
 fun declare_ext_elem prep_fixes (ctxt, Fixes fixes) =